Pure type systems without explicit contexts

DOI10.4204/EPTCS.34.6MaRDI QIDQ6941739zbMATH OpenFDO

Authors Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk

Publication date 19 August 2025

Copyright license Creative Commons license

Full work available at URL https://doi.org/10.4204/EPTCS.34.6

Mathematics Subject Classification ID

Type theory (03B38)

Cites work

• scientific article; zbMATH DE number 193320 (Why is no real title available?)
• scientific article; zbMATH DE number 512787 (Why is no real title available?)
• scientific article; zbMATH DE number 1499107 (Why is no real title available?)
• A formulation of the simple theory of types
• Closure under alpha-conversion
• Edinburgh LCF. A mechanized logic of computation
• Engineering formal metatheory
• Existential import revisited
• External and internal syntax of the \(\lambda \)-calculus
• Logic and structure
• Mathematical Knowledge Management
• Proof-assistants using dependent type systems
• Some lambda calculus and type theory formalized

Cited in

(1)

• Interacting safely with an unsafe environment

This page was built for publication: Pure type systems without explicit contexts

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6941739)