Erasure and Polymorphism in Pure Type Systems

DOI10.1007/978-3-540-78499-9_25MaRDI QIDQ5458371zbMATH OpenOpenAlexFDO

Authors Nathan Mishra-Linger, Tim Sheard

Publication date 11 April 2008

Published in Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78499-9_25

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Intensional polymorphism in type-erasure semantics
• Intensional polymorphism in type-erasure semantics
• Intensional polymorphism in type-erasure semantics
• Remarks on the equational theory of non-normalizing pure type systems
• Remarks on the equational theory of non-normalizing pure type systems

Cited in

(9)

• A type-assignment of linear erasure and duplication
• Attributive Types for Proof Erasure
• Foundations of dependent interoperability
• scientific article; zbMATH DE number 910819 (Why is no real title available?)
• Extracting functional programs from Coq, in Coq
• Intensional polymorphism in type-erasure semantics
• \(\eta\)-equivalence in core dependent Haskell
• Is Impredicativity Implicitly Implicit
• A dependent dependency calculus

Describes a project that uses

Uses Software

• Automath

This page was built for publication: Erasure and Polymorphism in Pure Type Systems

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