Pages that link to "Item:Q1823013"

The following pages link to The foundation of a generic theorem prover (Q1823013):

Displaying 50 items.

• Forum: A multiple-conclusion specification logic (Q671512) (← links)
• Using typed lambda calculus to implement formal systems on a machine (Q688571) (← links)
• Theo: An interactive proof development system (Q688727) (← links)
• A framework for proof systems (Q707742) (← links)
• Formal verification of C systems code. Structured types, separation logic and theorem proving (Q835768) (← links)
• TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
• A functional programming approach to the specification and verification of concurrent systems (Q909439) (← links)
• Term rewriting and beyond -- theorem proving in Isabelle (Q909488) (← links)
• A mechanized proof of the basic perturbation lemma (Q928666) (← links)
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms (Q964000) (← links)
• Program development in constructive type theory (Q1190474) (← links)
• Unification under a mixed prefix (Q1201348) (← links)
• Implementing tactics and tacticals in a higher-order logic programming language (Q1311396) (← links)
• Experimenting with Isabelle in ZF set theory (Q1312157) (← links)
• Set theory for verification. I: From foundations to functions (Q1319386) (← links)
• Inductive families (Q1336951) (← links)
• Program tactics and logic tactics (Q1380427) (← links)
• Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
• Program development schemata as derived rules (Q1583853) (← links)
• A semantic framework for proof evidence (Q1701039) (← links)
• TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
• A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
• Formalization of the Poincaré disc model of hyperbolic geometry (Q2031408) (← links)
• Isabelle's metalogic: formalization and proof checker (Q2055847) (← links)
• Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
• A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
• Generating custom set theories with non-set structured objects (Q2128829) (← links)
• From LCF to Isabelle/HOL (Q2280211) (← links)
• Term-generic logic (Q2339466) (← links)
• Fresh logic: Proof-theory and semantics for FM and nominal techniques (Q2372191) (← links)
• Automation for interactive proof: first prototype (Q2432769) (← links)
• Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started (Q2657827) (← links)
• A metatheory of a mechanized object theory (Q2676562) (← links)
• Encoding Generic Judgments (Q2841234) (← links)
• (Q4222859) (← links)
• A Shell for Generic Interactive Proof Search (Q4236062) (← links)
• (Q4499163) (← links)
• Computational logic: its origins and applications (Q4559535) (← links)
• R n - and G n -logics (Q4645806) (← links)
• Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology (Q4827602) (← links)
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf (Q4827615) (← links)
• Equivalences between logics and their representing type theories (Q4862761) (← links)
• Formalization of Forcing in Isabelle/ZF (Q5049004) (← links)
• An overview of LP, the Larch Prover (Q5055717) (← links)
• Rewriting, and equational unification: the higher-order cases (Q5055746) (← links)
• Higher-order superposition for dependent types (Q5055856) (← links)
• Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL (Q5094474) (← links)
• Proving and rewriting (Q5096184) (← links)
• (Q5140267) (← links)
• Mollusc a general proof-development shell for sequent-based logics (Q5210817) (← links)