scientific article; zbMATH DE number 2079014

MaRDI QIDQ4474826zbMATH OpenFDO

Authors D. Aspinall

Publication date 21 July 2004

Mathematics Subject Classification ID

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

Recommendations

• Strong normalization with singleton types
• Extensional equivalence and singleton types
• scientific article; zbMATH DE number 1670475
• Singleton, union and intersection types for program extraction
• Singleton, union, and intersection types for program extraction

Cited in

(13)

• Singleton, union, and intersection types for program extraction
• System ST toward a type system for extraction and proofs of programs
• Dependent types with subtyping and late-bound overloading
• Intersection and singleton type assignment characterizing finite Böhm-trees
• Strong normalization with singleton types
• A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
• Manifest Fields and Module Mechanisms in Intensional Type Theory
• Singleton, union and intersection types for program extraction
• Extensional equivalence and singleton types
• Dynamic translucency with abstraction kinds and higher-order coercions
• Subtyping dependent types
• Controlling unfolding in type theory
• Q\# as a quantum algorithmic language

This page was built for publication:

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