The calculus of constructions
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 4019061 (Why is no real title available?)
- scientific article; zbMATH DE number 3882404 (Why is no real title available?)
- scientific article; zbMATH DE number 3875278 (Why is no real title available?)
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 3928338 (Why is no real title available?)
- scientific article; zbMATH DE number 3928956 (Why is no real title available?)
- scientific article; zbMATH DE number 4058907 (Why is no real title available?)
- scientific article; zbMATH DE number 3657156 (Why is no real title available?)
- scientific article; zbMATH DE number 3684935 (Why is no real title available?)
- scientific article; zbMATH DE number 3735770 (Why is no real title available?)
- scientific article; zbMATH DE number 3485174 (Why is no real title available?)
- scientific article; zbMATH DE number 3513750 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 3521951 (Why is no real title available?)
- scientific article; zbMATH DE number 3280068 (Why is no real title available?)
- scientific article; zbMATH DE number 3328156 (Why is no real title available?)
- scientific article; zbMATH DE number 3331288 (Why is no real title available?)
- scientific article; zbMATH DE number 3349775 (Why is no real title available?)
- scientific article; zbMATH DE number 3400430 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- scientific article; zbMATH DE number 3085191 (Why is no real title available?)
- A unification algorithm for typed -calculus
- Combinators, \(\lambda\)-terms and proof theory
- Constructive mathematics and computer programming
- Edinburgh LCF. A mechanized logic of computation
- Progress report on generalized functionality
- Proof theory
- Semantics for classical AUTOMATH and related systems
- The lambda calculus, its syntax and semantics
Cited in
(only showing first 100 items - show all)- Intuitionistic completeness of first-order logic
- Proof-irrelevance out of excluded-middle and choice in the calculus of constructions
- Proof search with set variable instantiation in the calculus of constructions
- Composition of deductions within the propositions-as-types paradigm
- A First Look into a Formal and Constructive Approach for Discrete Geometry Using Nonstandard Analysis
- Higher order disunification: some decidable cases
- Normalising the associative law: An experiment with Martin-Löf's type theory
- A formal semantics of nested atomic sections with thread escape
- On the proof theory of Coquand's calculus of constructions
- Third-order matching in the polymorphic lambda calculus
- Characteristics of de Bruijn’s early proof checker Automath
- Twenty years of rewriting logic
- A logical framework combining model and proof theory
- Formally verifying the solution to the Boolean Pythagorean triples problem
- High-Level Theories
- Constructive game logic
- On the compatibility between the minimalist foundation and constructive set theory
- New Curry-Howard terms for full linear logic
- Insight in discrete geometry and computational content of a discrete model of the continuum
- Polymorphic rewriting conserves algebraic strong normalization
- Automorphisms of types in certain type theories and representation of finite groups
- A scalable module system
- Singleton, union and intersection types for program extraction
- Revisiting the notion of function
- Program specification and data refinement in type theory
- An analysis of Tennenbaum's theorem in constructive type theory
- scientific article; zbMATH DE number 1405632 (Why is no real title available?)
- Extending type theory with forcing
- A modular coding of \textsc{Unity} in \textsc{Coq}
- A unified approach to type theory through a refined -calculus
- Programming by example and proving by example using higher-order unification
- PML2: integrated program verification in ML
- scientific article; zbMATH DE number 7559280 (Why is no real title available?)
- Categorical abstract machines for higher-order typed -calculi
- Adding algebraic rewriting to the untyped lambda calculus
- An Evaluation of Automata Algorithms for String Analysis
- A certified, corecursive implementation of exact real numbers
- scientific article; zbMATH DE number 7779294 (Why is no real title available?)
- Representing model theory in a type-theoretical logical framework
- Type classes for mathematics in type theory
- The Impact of the Lambda Calculus in Logic and Computer Science
- Kinded type inference for parametric overloading
- The foundation of a generic theorem prover
- Independence of the induction principle and the axiom of choice in the pure calculus of constructions
- Constructive mathematics, Church's thesis, and free choice sequences
- The seven virtues of simple type theory
- scientific article; zbMATH DE number 7552282 (Why is no real title available?)
- Modularity of termination and confluence in combinations of rewrite systems with \(\lambda_\omega\)
- The formal verification of the ctm approach to forcing
- scientific article; zbMATH DE number 4191621 (Why is no real title available?)
- Mechanized metatheory revisited
- Graded modal dependent type theory
- Types for the ambient calculus
- A framework for defining logical frameworks
- Programmed strategies for program verification
- Interpreting HOL in the calculus of constructions
- Variants of the basic calculus of constructions
- Axiomatization of calculus of constructions
- Material dialogues for first-order logic in constructive type theory
- Using formal methods with SysML in aerospace design and engineering
- Incorporating quotation and evaluation into Church's type theory
- Constructing type systems over an operational semantics
- From constructivism to computer science
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification
- An induction principle for pure type systems
- Algebra of constructions II: an algebraic approach to Martin-Löf type theory and the calculus of constructions
- An application of PER models to program extraction
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- Type theories from Barendregt's cube for theorem provers
- Extensional proofs in a propositional logic modulo isomorphisms
- Flexary operators for formalized mathematics
- Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory
- A natural deduction approach to dynamic logic
- Type theory as a foundation for computer science
- The extended calculus of constructions (ECC) with inductive types
- Mathesis Universalis and Homotopy Type Theory
- Universal properties for universal types in bifibrational parametricity
- From realizability to induction via dependent intersection
- Formal verification of a leader election protocol in process algebra
- A notation for lambda terms. A generalization of environments
- Reflection of formal tactics in a deductive reflection framework
- An intuitionistic set-theoretical model of fully dependent CC
- Logic of refinement types
- Theoretical computer science: computability, decidability and logic
- Annual Meeting of the Association for Symbolic Logic, Los Angeles, 1989
- Native type theory
- Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
- Pure type systems with more liberal rules
- Formalising overlap algebras in Matita
- A classical sequent calculus with dependent types
- Higher-order substitutions
- From mathesis universalis to provability, computability, and constructivity
- The Girard-Reynolds isomorphism (second edition)
- Inductive families
- Telescopic mappings in typed lambda calculus
- Unified syntax with iso-types
- Toward formal development of programs from algebraic specifications: Parameterisation revisited
- An approach to literate and structured formal developments
- Constructive and mechanised meta-theory of intuitionistic epistemic logic
- Modular dependent induction in Coq, Mendler-style
This page was built for publication: The calculus of constructions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1108266)
