From realizability to induction via dependent intersection

DOI10.1016/j.apal.2018.03.002zbMath1469.03037OpenAlexW2793739232WikidataQ130126025 ScholiaQ130126025MaRDI QIDQ2636522

Aaron Stump

Publication date: 5 June 2018

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2018.03.002

zbMATH Keywords

derivable inductionextrinsic typinginternalized realizabilitylambda encodings

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40) Type theory (03B38)

Related Items (2)

Monotone recursive types and recursive data representations in Cedille ⋮ Unnamed Item

Uses Software

• Coq
• Automath
• Agda

Cites Work

• 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
• The calculus of constructions
• Well-ordering proofs for Martin-Löf type theory
• Efficient Mendler-style lambda-encodings in Cedille
• Type Theory Should Eat Itself
• Type theory in type theory using quotient inductive types
• Conventional Necessity and the Contingency of Convention
• A Categorical Semantics for Inductive-Inductive Definitions
• ΠΣ: Dependent Types without the Sugar
• Fibrational Induction Rules for Initial Algebras
• The Expressiveness of Simple and Second-Order Type Structures
• Every planar map is four colorable
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Internal type theory
• Functionality in Combinatory Logic
• Efficient self-interpretation in lambda calculus
• Intersection Types from a Proof-theoretic Perspective
• The gentle art of levitation
• Efficiency of lambda-encodings in total type theory
• The calculus of dependent lambda eliminations
• Special issue on Programming with Dependent Types Editorial
• A relationally parametric model of dependent type theory
• Inductively defined types in the Calculus of Constructions

This page was built for publication: From realizability to induction via dependent intersection