Strong normalization with singleton types

DOI10.1016/S1571-0661(04)80490-0MaRDI QIDQ2842835zbMATH OpenFDO

Authors Judicaël Courant

Publication date 16 August 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S1571-0661(04)80490-0

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2079014
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Strong normalization in core type theory
• scientific article; zbMATH DE number 1943083
• Extensional equivalence and singleton types

Cites work

• (In)consistency of Extensions of Higher Order Logic and Type Theory
• Deciding type equivalence in a language with singleton kinds
• Geometric methods and applications. For computer science and engineering
• scientific article; zbMATH DE number 2185661 (Why is no real title available?)
• scientific article; zbMATH DE number 2079014 (Why is no real title available?)
• Parallel reductions in \(\lambda\)-calculus
• Typed operational semantics for higher-order subtyping.

Cited in

(5)

• System ST toward a type system for extraction and proofs of programs
• scientific article; zbMATH DE number 2079014 (Why is no real title available?)
• scientific article; zbMATH DE number 1746455 (Why is no real title available?)
• Extensional equivalence and singleton types
• Sound and complete elimination of singleton kinds

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Strong normalization with singleton types

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