Inductively defined types in the Calculus of Constructions

DOI10.1007/BFb0040259OpenAlexW1852211073MaRDI QIDQ5887516

Christine Paulin-Mohring, Frank Pfenning

Publication date: 12 April 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bfb0040259

zbMATH Keywords

lambda calculusinduction principleinductive definitioninductive typedependent pair

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (13)

From realizability to induction via dependent intersection ⋮ Monotone recursive definition of predicates and its realizability interpretation ⋮ Expressing computational complexity in constructive type theory ⋮ The formal verification of the ctm approach to forcing ⋮ Cut elimination for a logic with induction and co-induction ⋮ A henkin-style completeness proof for the modal logic S5 ⋮ Unnamed Item ⋮ The calculus of dependent lambda eliminations ⋮ Metacircularity in the polymorphic \(\lambda\)-calculus ⋮ Least and greatest fixed points in intuitionistic natural deduction ⋮ A note on complexity measures for inductive classes in constructive type theory ⋮ Type Theories from Barendregt’s Cube for Theorem Provers ⋮ Deciding Kleene algebra terms equivalence in Coq

Uses Software

• Automath

Cites Work

• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• The calculus of constructions
• The Expressiveness of Simple and Second-Order Type Structures
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Inductively defined types in the Calculus of Constructions