The following pages link to (Q5687569):
Displaying 45 items.
- Mechanised support for sound refinement tactics (Q432151) (← links)
- Exploring structural symmetry automatically in symbolic trajectory evaluation (Q453494) (← links)
- An inductive approach to strand spaces (Q470008) (← links)
- A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL (Q541222) (← links)
- Reasoning about conditional probabilities in a higher-order-logic theorem prover (Q545151) (← links)
- Formal reliability analysis of combinational circuits using theorem proving (Q545153) (← links)
- Specifying rewrite strategies for interactive exercises (Q626940) (← links)
- On the role of memory in object-based and object-oriented languages (Q674010) (← links)
- Should ML be object-oriented? (Q699925) (← links)
- Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation (Q782499) (← links)
- Providing a formal linkage between MDG and HOL (Q878110) (← links)
- A few exercises in theorem processing (Q879370) (← links)
- Formalization of the standard uniform random variable (Q995466) (← links)
- Using theorem proving to verify expectation and variance for discrete random variables (Q1040780) (← links)
- A notation for lambda terms. A generalization of environments (Q1129257) (← links)
- A co-induction principle for recursively defined domains (Q1318702) (← links)
- Deductive and inductive synthesis of equational programs (Q1322836) (← links)
- PCF extended with real numbers (Q1349926) (← links)
- Essential concepts of algebraic specification and program development (Q1377322) (← links)
- The definition of Extended ML: A gentle introduction (Q1391731) (← links)
- Formal analysis of continuous-time systems using Fourier transform (Q1640640) (← links)
- Modeling message queueing services with reliability guarantee in cloud computing environment using colored Petri nets (Q1665556) (← links)
- Amalgamation in the semantics of CASL (Q1770431) (← links)
- Organizing numerical theories using axiomatic type classes (Q1774558) (← links)
- A tactic calculus. --- Abridged version (Q1815345) (← links)
- Mechanising the theory of intervals using OBJ3 (Q1916976) (← links)
- Unifying theories in ProofPower-Z (Q1941892) (← links)
- The locally nameless representation (Q1945914) (← links)
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (Q1945915) (← links)
- Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light} (Q2198134) (← links)
- Priority inheritance protocol proved correct (Q2303234) (← links)
- Proof pearl: A mechanized proof of GHC's mergesort (Q2351394) (← links)
- On the formalization of gamma function in HOL (Q2352499) (← links)
- Types for modules (Q2375744) (← links)
- Decidability of bounded higher-order unification (Q2456577) (← links)
- Shallow confluence of conditional term rewriting systems (Q2518609) (← links)
- Compensation methods to support cooperative applications: A case study in automated verification of schema requirements for an advanced transaction model (Q2744791) (← links)
- The Orc Programming Language (Q3634722) (← links)
- Demonstrating Lambda Calculus Reduction (Q4917067) (← links)
- Pixel Geometry (Q4923377) (← links)
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus (Q4972064) (← links)
- F-ing modules (Q4983210) (← links)
- A fixedpoint approach to implementing (Co)inductive definitions (Q5210768) (← links)
- Evaluation of anonymity and confidentiality protocols using theorem proving (Q5962971) (← links)
- Reductive logic, proof-search, and coalgebra: a perspective from resource semantics (Q6612799) (← links)
