Pure type system conversion is always typable

DOI10.1017/S0956796812000044zbMATH Open1271.68080MaRDI QIDQ2844696FDOQ2844696

Authors: Vincent Siles, Hugo Herbelin 

Publication date: 19 August 2013

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

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

zbMATH Keywords

functional pure type systems

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cites Work

• Title not available (Why is that?)
• Pure type systems with judgemental equality

Cited In (11)

• An adequacy theorem for dependent type theory
• Canonical typing and ∏-conversion in the Barendregt Cube
• Pure type systems with judgemental equality
• 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
• Title not available (Why is that?)

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)