The following pages link to The calculus of constructions (Q1108266):
Displaying 50 items.
- The calculus of constructions as a framework for proof search with set variable instantiation (Q1575927) (← links)
- Search algorithms in type theory (Q1575934) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- \(\pi\)-calculus in (Co)inductive-type theory (Q1589654) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- A formal semantics of nested atomic sections with thread escape (Q1749114) (← links)
- Incorporating quotation and evaluation into Church's type theory (Q1753993) (← links)
- The foundation of a generic theorem prover (Q1823013) (← links)
- On the logic of unification (Q1823935) (← links)
- Higher-order substitutions (Q1854398) (← links)
- Variants of the basic calculus of constructions (Q1885480) (← links)
- The Girard-Reynolds isomorphism (Q1887154) (← links)
- On completeness and cocompleteness in and around small categories (Q1896485) (← links)
- Kinded type inference for parametric overloading (Q1911131) (← links)
- An approach to literate and structured formal developments (Q1911317) (← links)
- TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
- Type-specialized staged programming with process separation (Q1929349) (← links)
- Twenty years of rewriting logic (Q1931904) (← links)
- N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker (Q1935352) (← links)
- Certifying Findel derivatives for blockchain (Q2043802) (← links)
- The Lean 4 theorem prover and programming language (Q2055901) (← links)
- Predicativity and constructive mathematics (Q2080590) (← links)
- Constructive hybrid games (Q2096468) (← links)
- On the compatibility between the minimalist foundation and constructive set theory (Q2104267) (← links)
- Constructive mathematics, Church's thesis, and free choice sequences (Q2117809) (← links)
- Voting theory in the Lean theorem prover (Q2148823) (← links)
- Constructive and mechanised meta-theory of intuitionistic epistemic logic (Q2151399) (← links)
- Composition of deductions within the propositions-as-types paradigm (Q2228351) (← links)
- Graded modal dependent type theory (Q2233475) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Formally verifying the solution to the Boolean Pythagorean triples problem (Q2323449) (← links)
- Deciding Kleene algebra terms equivalence in Coq (Q2347910) (← links)
- Types for the ambient calculus (Q2497144) (← links)
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification (Q2629858) (← links)
- From realizability to induction via dependent intersection (Q2636522) (← links)
- A higher-order calculus and theory abstraction (Q2639838) (← links)
- A bi-directional extensible interface between Lean and Mathematica (Q2673306) (← links)
- A henkin-style completeness proof for the modal logic S5 (Q2695534) (← links)
- (Q2703692) (← links)
- A Classical Realizability Model for a Semantical Value Restriction (Q2802494) (← links)
- Another Look at Function Domains (Q2805150) (← links)
- Modular Dependent Induction in Coq, Mendler-Style (Q2829276) (← links)
- Certifying Term Rewriting Proofs in ELAN (Q2841249) (← links)
- A Framework for Defining Logical Frameworks (Q2864157) (← links)
- Programmed Strategies for Program Verification (Q2864527) (← links)
- Computerizing Mathematical Text with MathLang (Q2866734) (← links)
- Inductive and Coinductive Components of Corecursive Functions in Coq (Q2873661) (← links)
- Proof-producing translation of higher-order logic into pure and stateful ML (Q2875232) (← links)
- Homotopy type theory and Voevodsky’s univalent foundations (Q2933829) (← links)
- Parametric Polymorphism — Universally (Q2947462) (← links)
