The following pages link to (Q5417200):
Displaying 44 items.
- Coq (Q12929) (← links)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (Q703860) (← links)
- Implementing geometric algebra products with binary trees (Q742367) (← links)
- Mechanizing type environments in weak HOAS (Q897934) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Bellerophon: tactical theorem proving for hybrid systems (Q1687737) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- Bestow and atomic: concurrent programming using isolation, delegation and grouping (Q1785860) (← links)
- A certified program for the Karatsuba method to multiply polynomials (Q2132545) (← links)
- On a machine-checked proof for fraction arithmetic over a GCD domain (Q2217198) (← links)
- Fifty years of Hoare's logic (Q2280214) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective (Q2354911) (← links)
- Proof mining with dependent types (Q2364689) (← links)
- Automatically proving equivalence by type-safe reflection (Q2364699) (← links)
- System-level non-interference of constant-time cryptography. I: Model (Q2417947) (← links)
- Consistency-preserving refactoring of refinement structures in Event-B models (Q2418044) (← links)
- Proof-assistants using dependent type systems (Q2751370) (← links)
- Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics (Q2817296) (← links)
- Verified Operational Transformation for Trees (Q2829271) (← links)
- Homotopy type theory and Voevodsky’s univalent foundations (Q2933829) (← links)
- Auto in Agda (Q2941181) (← links)
- Friends with Benefits (Q2988636) (← links)
- (Q4428314) (← links)
- Applicable Mathematics in a Minimal Computational Theory of Sets (Q4553281) (← links)
- Foundations of dependent interoperability (Q4577812) (← links)
- (Q5015189) (← links)
- (Q5028488) (← links)
- A Formalization of Properties of Continuous Functions on Closed Intervals (Q5041063) (← links)
- Practical Proof Search for Coq by Type Inhabitation (Q5048991) (← links)
- ANF preserves dependent types up to extensional equality (Q5051989) (← links)
- Fold–unfold lemmas for reasoning about recursive programs using the Coq proof assistant (Q5051990) (← links)
- Verifying Selective CPS Transformation for Shift and Reset (Q5098734) (← links)
- Extracting functional programs from Coq, in Coq (Q5101927) (← links)
- (Q5109521) (← links)
- Formalizing Scientifically Applicable Mathematics in a Definitional Framework (Q5195269) (← links)
- (Q5216307) (← links)
- Mtac: A monad for typed tactic programming in Coq (Q5371944) (← links)
- The essence of ornaments (Q5372005) (← links)
- (Q5875410) (← links)
- An automatically verified prototype of the Android permissions system (Q6103592) (← links)
- Recursion schemes in Coq (Q6536316) (← links)
- Topological quantum gates in homotopy type theory (Q6584358) (← links)
- Formal definitions and proofs for partial (co)recursive functions (Q6615564) (← links)
