The calculus of constructions
From MaRDI portal
Publication:1108266
DOI10.1016/0890-5401(88)90005-3zbMath0654.03045OpenAlexW1986402635WikidataQ56385237 ScholiaQ56385237MaRDI QIDQ1108266
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
mechanized mathematicsfunctional systemrealizability interpretationAutomathimpredicative extension of Martin-Löf type theorytype system for functional programminguntyped \(\lambda \) -calculus
General topics in the theory of software (68N01) Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)
Related Items (only showing first 100 items - show all)
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
Uses Software
Cites Work
- The lambda calculus, its syntax and semantics
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Edinburgh LCF. A mechanized logic of computation
- Combinators, \(\lambda\)-terms and proof theory
- Constructive mathematics and computer programming
- Semantics for classical AUTOMATH and related systems
- Progress report on generalized functionality
- Proof theory
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: The calculus of constructions
