The following pages link to The calculus of constructions (Q1108266):
Displaying 50 items.
- Bridging Curry and Church's typing style (Q334149) (← links)
- A two-valued logic for properties of strict functional programs allowing partial functions (Q352946) (← links)
- A scalable module system (Q391632) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Using formal methods with SysML in aerospace design and engineering (Q434438) (← links)
- Binary trees as a computational framework (Q461478) (← links)
- Flag-based big-step semantics (Q516041) (← links)
- Preface to the special volume (Q534064) (← links)
- Independence results in formal topology (Q651321) (← links)
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus (Q672060) (← links)
- Using typed lambda calculus to implement formal systems on a machine (Q688571) (← links)
- The semantics of second-order lambda calculus (Q751294) (← links)
- Telescopic mappings in typed lambda calculus (Q757027) (← links)
- Extraction of redundancy-free programs from constructive natural deduction proofs (Q808284) (← links)
- Normalising the associative law: An experiment with Martin-Löf's type theory (Q809071) (← links)
- A certified, corecursive implementation of exact real numbers (Q817858) (← links)
- An epistemic logic for becoming informed (Q833038) (← links)
- Insight in discrete geometry and computational content of a discrete model of the continuum (Q834257) (← links)
- Choices in representation and reduction strategies for lambda terms in intensional contexts (Q861365) (← links)
- The Girard-Reynolds isomorphism (second edition) (Q879366) (← links)
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← links)
- The seven virtues of simple type theory (Q946569) (← links)
- A computer-verified monadic functional implementation of the integral (Q987984) (← links)
- Certifying properties of an efficient functional program for computing Gröbner bases (Q1012152) (← links)
- A notation for lambda terms. A generalization of environments (Q1129257) (← links)
- Inheritance as implicit coercion (Q1175335) (← links)
- Polymorphic rewriting conserves algebraic strong normalization (Q1176244) (← links)
- Metacircularity in the polymorphic \(\lambda\)-calculus (Q1177938) (← links)
- Program development in constructive type theory (Q1190474) (← links)
- New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic (Q1193588) (← links)
- The extended calculus of constructions (ECC) with inductive types (Q1193601) (← links)
- Independence of the induction principle and the axiom of choice in the pure calculus of constructions (Q1199547) (← links)
- Constructing type systems over an operational semantics (Q1199709) (← links)
- Coquand's calculus of constructions: A mathematical foundation for a proof development system (Q1201296) (← links)
- Adding algebraic rewriting to the untyped lambda calculus (Q1207945) (← links)
- From constructivism to computer science (Q1274450) (← links)
- Implementing tactics and tacticals in a higher-order logic programming language (Q1311396) (← links)
- IMPS: An interactive mathematical proof system (Q1319391) (← links)
- Combining type disciplines (Q1319505) (← links)
- \(QPC_ 2\): A constructive calculus with parameterized specifications (Q1322848) (← links)
- Toward formal development of programs from algebraic specifications: Parameterisation revisited (Q1323357) (← links)
- Inductive families (Q1336951) (← links)
- Categorical abstract machines for higher-order typed \(\lambda\)-calculi (Q1349667) (← links)
- A unified approach to type theory through a refined \(\lambda\)-calculus (Q1349674) (← links)
- Formalizing process algebraic verifications in the calculus of constructions (Q1355748) (← links)
- Comparing cubes of typed and type assignment systems (Q1365249) (← links)
- New Curry-Howard terms for full linear logic (Q1390952) (← links)
- Formal verification of a leader election protocol in process algebra (Q1391796) (← links)
- Revisiting the notion of function (Q1394989) (← links)
