scientific article; zbMATH DE number 4189687

zbMath0722.03006MaRDI QIDQ5753923

Thierry Coquand, Christine Paulin

Publication date: 1990

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

recursion operatorshigher-order logictype theoryinduction principlesinductively defined typesconcrete data typesextension of Church's simple type theoryproposition-as- types

Mathematics Subject Classification ID

Related Items (49)

Inductive families ⋮ Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis ⋮ From realizability to induction via dependent intersection ⋮ Formalizing process algebraic verifications in the calculus of constructions ⋮ A higher-order calculus and theory abstraction ⋮ A two-level logic approach to reasoning about computations ⋮ Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ Trusting computations: a mechanized proof from partial differential equations to actual program ⋮ Procedural representation of CIC proof terms ⋮ Constructive sheaf models of type theory ⋮ Size-based termination of higher-order rewriting ⋮ Intuitionistic completeness of first-order logic ⋮ A bi-directional extensible interface between Lean and Mathematica ⋮ Representing inductively defined sets by wellorderings in Martin-Löf's type theory ⋮ Completeness and expressiveness of pointer program verification by separation logic ⋮ Formal categorical reasoning ⋮ The metatheory of UTT ⋮ What is the point of computers? A question for pure mathematicians ⋮ Induction-recursion and initial algebras. ⋮ The calculus of dependent lambda eliminations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On Choice Rules in Dependent Type Theory ⋮ A Short Presentation of Coq ⋮ Formalizing non-interference for a simple bytecode language in Coq ⋮ Metacircularity in the polymorphic \(\lambda\)-calculus ⋮ Impossibility of gathering, a certification ⋮ A Type-Theoretic Framework for Certified Model Transformations ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ The extended calculus of constructions (ECC) with inductive types ⋮ Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice ⋮ Realizability models and implicit complexity ⋮ The undecidability of pattern matching in calculi where primitive recursive functions are representable ⋮ Logic of subtyping ⋮ A computer-verified monadic functional implementation of the integral ⋮ Inductive-data-type systems ⋮ Least and greatest fixed points in intuitionistic natural deduction ⋮ Computer Certified Efficient Exact Reals in Coq ⋮ Synchronous gathering without multiplicity detection: a certified algorithm ⋮ Certifying Findel derivatives for blockchain ⋮ Implementing geometric algebra products with binary trees ⋮ High-Level Theories ⋮ Type Theories from Barendregt’s Cube for Theorem Provers ⋮ Constructive hybrid games ⋮ Indexed induction-recursion ⋮ Automata-driven automated induction ⋮ Cogent: uniqueness types and certifying compilation ⋮ Synthesis of ML programs in the system Coq ⋮ On modal logics of partial recursive functions

This page was built for publication: