Pure type system conversion is always typable

DOI10.1017/S0956796812000044MaRDI QIDQ2844696zbMATH OpenFDO

Authors Vincent Siles, Hugo Herbelin

Publication date 19 August 2013

Published in Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

functional pure type systems

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Pure type systems with judgemental equality
• Pure type systems with explicit substitutions
• Typing in pure type systems
• scientific article; zbMATH DE number 1222569
• Equivalences between pure type systems and systems of illative combinatory logic

Cites work

• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• Pure type systems with judgemental equality

Cited in

(11)

• scientific article; zbMATH DE number 65534 (Why is no real title available?)
• An adequacy theorem for dependent type theory
• Pure type systems with judgemental equality
• Canonical typing and ∏-conversion in the Barendregt Cube
• Pure subtype systems
• An induction principle for pure type systems
• Pure type systems with explicit substitutions
• Are there Hilbert-style Pure Type Systems?
• Normalization by Evaluation for Typed Weak lambda-Reduction
• From rewrite rules to axioms in the \(\lambda \varPi \)-calculus modulo theory
• Cumulative inductive types in Coq

This page was built for publication: Pure type system conversion is always typable

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