Pure type systems with judgemental equality

DOI10.1017/S0956796805005770zbMATH Open1088.68030MaRDI QIDQ3377462FDOQ3377462

Authors: Robin Adams 

Publication date: 22 March 2006

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

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

zbMATH Keywords

Church-Rosser theoremuniqueness of types

Mathematics Subject Classification ID

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

Cited In (10)

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

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)