The calculus of constructions

From MaRDI portal

Publication:1108266

Jump to:navigation, search

DOI10.1016/0890-5401(88)90005-3zbMath0654.03045OpenAlexW1986402635WikidataQ56385237 ScholiaQ56385237MaRDI QIDQ1108266

Gérard Huet, Thierry Coquand

Publication date: 1988

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(88)90005-3

zbMATH Keywords

mechanized mathematics functional system realizability interpretation Automath impredicative extension of Martin-Löf type theory type system for functional programming untyped \(\lambda \) -calculus

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)

Related Items

Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved, Differential Game Logic, A modular construction of type theories, Inductively defined types in the Calculus of Constructions, Constructive Game Logic, Semantic Foundations for Deterministic Dataflow and Stream Processing, Applications of type theory, Validating Mathematical Structures, ANF preserves dependent types up to extensional equality, Unnamed Item, The Lean Theorem Prover (System Description), Adding algebraic rewriting to the untyped lambda calculus (extended abstract), Unified Syntax with Iso-types, A Brief Overview of Agda – A Functional Language with Dependent Types, 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, Program specification and data refinement in type theory, Proof-Relevant Parametricity, Computational logic: its origins and applications, Annual Meeting of the Association for Symbolic Logic, Los Angeles, 1989, Characteristics of de Bruijn’s early proof checker Automath, Unnamed Item, Type theory as a foundation for computer science, Singleton, union and intersection types for program extraction, Higher order disunification: Some decidable cases, Quotients by Idempotent Functions in Cedille, Extensional proofs in a propositional logic modulo isomorphisms, Proving strong normalization of CC by modifying realizability semantics, Checking algorithms for Pure Type Systems, Conservativity between logics and typed λ calculi, Logic of refinement types, The Alf proof editor and its proof engine, Semantics for abstract clauses, A short and flexible proof of strong normalization for the calculus of constructions, Embedding \(\mathsf{HTLCG}\) into \(\mathsf{LCG}_\phi \), An automatically verified prototype of the Android permissions system, The compatibility of the minimalist foundation with homotopy type theory, The formal verification of the ctm approach to forcing, Material dialogues for first-order logic in constructive type theory, An intuitionistic set-theoretical model of fully dependent CC, Pure type systems with more liberal rules, Strong normalisation in two Pure Pattern Type Systems, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Universal properties for universal types in bifibrational parametricity, Unnamed Item, On cubism, Proof-irrelevance out of excluded-middle and choice in the calculus of constructions, Unnamed Item, A Classical Sequent Calculus with Dependent Types, A Short Presentation of Coq, A Type of Partial Recursive Functions, Modularity of termination and confluence in combinations of rewrite systems with λω, The Impact of the Lambda Calculus in Logic and Computer Science, Type theoretic semantics for SemNet, Mathesis Universalis and Homotopy Type Theory, From Mathesis Universalis to Provability, Computability, and Constructivity, A logical framework combining model and proof theory, Third-order matching in the polymorphic lambda calculus, Reflection of formal tactics in a deductive reflection framework, Proof search with set variable instantiation in the Calculus of Constructions, Automating inversion of inductive predicates in Coq, A natural deduction approach to dynamic logic, Proof normalization modulo, An Interactive Driver for Goal-directed Proof Strategies, Semantics of constructions. I: The traditional approach, An experimental library of formalized Mathematics based on the univalent foundations, Partiality and recursion in interactive theorem provers – an overview, A higher-order interpretation of deductive tableau, A case-study in algebraic manipulation using mechanized reasoning tools, Semantics of constructions. II: The initial algebraic approach, A partial functions version of Church's simple theory of types, Intuitionistic categorial grammar, Unnamed Item, Unnamed Item, Unnamed Item, Subtyping dependent types, Proof-term synthesis on dependent-type systems via explicit substitutions, An induction principle for pure type systems, Computer Certified Efficient Exact Reals in Coq, On the proof theory of Coquand's calculus of constructions, A First Look into a Formal and Constructive Approach for Discrete Geometry Using Nonstandard Analysis, An Evaluation of Automata Algorithms for String Analysis, Formalising Overlap Algebras in Matita, Type classes for mathematics in type theory, Formalising foundations of mathematics, A pluralist approach to the formalisation of mathematics, Flexary Operators for Formalized Mathematics, Automorphisms of types in certain type theories and representation of finite groups, High-Level Theories, Type Theories from Barendregt’s Cube for Theorem Provers, Program Testing and the Meaning Explanations of Intuitionistic Type Theory, Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code, Inductive families, An epistemic logic for becoming informed, Insight in discrete geometry and computational content of a discrete model of the continuum, Variants of the basic calculus of constructions, Unnamed Item, The Girard-Reynolds isomorphism, Synthesis of positive logic programs for checking a class of definitions with infinite quantification, Categorical abstract machines for higher-order typed \(\lambda\)-calculi, A unified approach to type theory through a refined \(\lambda\)-calculus, On completeness and cocompleteness in and around small categories, From realizability to induction via dependent intersection, Voting theory in the Lean theorem prover, Formalizing process algebraic verifications in the calculus of constructions, A higher-order calculus and theory abstraction, Constructive and mechanised meta-theory of intuitionistic epistemic logic, Bridging Curry and Church's typing style, Choices in representation and reduction strategies for lambda terms in intensional contexts, Comparing cubes of typed and type assignment systems, Kinded type inference for parametric overloading, An approach to literate and structured formal developments, A two-valued logic for properties of strict functional programs allowing partial functions, Hammer for Coq: automation for dependent type theory, Homotopy type theory and Voevodsky’s univalent foundations, The Girard-Reynolds isomorphism (second edition), TPS: A theorem-proving system for classical type theory, A notation for lambda terms. A generalization of environments, A scalable module system, Type-specialized staged programming with process separation, Intuitionistic completeness of first-order logic, Parametric Polymorphism — Universally, A bi-directional extensible interface between Lean and Mathematica, New Curry-Howard terms for full linear logic, Formal verification of a leader election protocol in process algebra, Twenty years of rewriting logic, Revisiting the notion of function, N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, Using formal methods with SysML in aerospace design and engineering, A henkin-style completeness proof for the modal logic S5, Independence results in formal topology, Binary trees as a computational framework, Representing model theory in a type-theoretical logical framework, Inheritance as implicit coercion, Polymorphic rewriting conserves algebraic strong normalization, Metacircularity in the polymorphic \(\lambda\)-calculus, Composition of deductions within the propositions-as-types paradigm, Graded modal dependent type theory, Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus, The seven virtues of simple type theory, Program development in constructive type theory, New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic, The extended calculus of constructions (ECC) with inductive types, A formal semantics of nested atomic sections with thread escape, Flag-based big-step semantics, Independence of the induction principle and the axiom of choice in the pure calculus of constructions, Constructing type systems over an operational semantics, Incorporating quotation and evaluation into Church's type theory, Coquand's calculus of constructions: A mathematical foundation for a proof development system, Using typed lambda calculus to implement formal systems on a machine, Preface to the special volume, Adding algebraic rewriting to the untyped lambda calculus, Types for the ambient calculus, A computer-verified monadic functional implementation of the integral, A Classical Realizability Model for a Semantical Value Restriction, Another Look at Function Domains, Certifying Findel derivatives for blockchain, Certifying properties of an efficient functional program for computing Gröbner bases, The semantics of second-order lambda calculus, The Lean 4 theorem prover and programming language, Telescopic mappings in typed lambda calculus, From constructivism to computer science, Modular Dependent Induction in Coq, Mendler-Style, The foundation of a generic theorem prover, On the logic of unification, Mechanized metatheory revisited, Formally verifying the solution to the Boolean Pythagorean triples problem, Certifying Term Rewriting Proofs in ELAN, The calculus of constructions as a framework for proof search with set variable instantiation, Search algorithms in type theory, Proof-search in type-theoretic languages: An introduction, Predicativity and constructive mathematics, \(\pi\)-calculus in (Co)inductive-type theory, Constructive hybrid games, Higher-order substitutions, A Framework for Defining Logical Frameworks, Programmed Strategies for Program Verification, Implementing tactics and tacticals in a higher-order logic programming language, On the compatibility between the minimalist foundation and constructive set theory, Computerizing Mathematical Text with MathLang, Deciding Kleene algebra terms equivalence in Coq, Extraction of redundancy-free programs from constructive natural deduction proofs, Normalising the associative law: An experiment with Martin-Löf's type theory, Inductive and Coinductive Components of Corecursive Functions in Coq, IMPS: An interactive mathematical proof system, Combining type disciplines, Proof-producing translation of higher-order logic into pure and stateful ML, \(QPC_ 2\): A constructive calculus with parameterized specifications, Toward formal development of programs from algebraic specifications: Parameterisation revisited, Constructive mathematics, Church's thesis, and free choice sequences, A certified, corecursive implementation of exact real numbers

Uses Software

Automath

Cites Work

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:1108266&oldid=13147853"