Pure Type System conversion is always typable
From MaRDI portal
Publication:2844696
DOI10.1017/S0956796812000044zbMath1271.68080MaRDI QIDQ2844696
Publication date: 19 August 2013
Published in: Journal of Functional Programming (Search for Journal in Brave)
Related Items (4)
Pure type systems with explicit substitutions ⋮ Cumulative Inductive Types in Coq ⋮ An adequacy theorem for dependent type theory ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction
Cites Work
This page was built for publication: Pure Type System conversion is always typable
