Pure type systems with judgemental equality

DOI10.1017/S0956796805005770MaRDI QIDQ3377462zbMATH OpenFDO

Authors Robin Adams

Publication date 22 March 2006

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

Full work available at URL https://doi.org/10.1017/S0956796805005770

zbMATH Keywords

Church-Rosser theoremuniqueness of types

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• Pure type system conversion is always typable
• Typing in pure type systems
• Soundness of Coercion in the Calculus of Constructions
• Foundations of Software Science and Computational Structures
• On the conservativity of Leibniz equality

Cited in

(10)

• An adequacy theorem for dependent type theory
• Pure type system conversion is always typable
• A logical framework with explicit conversions
• Unified syntax with iso-types
• I got plenty o' nuttin'
• scientific article; zbMATH DE number 4180818 (Why is no real title available?)
• On the conservativity of Leibniz equality
• Pure type systems with explicit substitutions
• \(\eta\)-equivalence in core dependent Haskell
• From rewrite rules to axioms in the \(\lambda \varPi \)-calculus modulo theory

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Pure type systems with judgemental equality

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