Free theorems and runtime type representations

DOI10.1016/J.ENTCS.2007.02.043MaRDI QIDQ5262947zbMATH OpenOpenAlexFDO

Authors Dimitrios Vytiniotis, Stephanie Weirich

Publication date 10 July 2015

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

Full work available at URL https://doi.org/10.1016/j.entcs.2007.02.043

zbMATH Keywords

polymorphismlogical relationsparametricityGADTstype representations

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65)

Recommendations

• Parametricity, type equality, and higher-order polymorphism
• Refined typing to localize the impact of forced strictness on free theorems
• Free theorems involving type constructor classes, functional pearl
• Free theorems in the presence of seq
• Formal parametric polymorphism

Cites work

• scientific article; zbMATH DE number 1693038 (Why is no real title available?)
• scientific article; zbMATH DE number 65535 (Why is no real title available?)
• scientific article; zbMATH DE number 1088048 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• scientific article; zbMATH DE number 2238212 (Why is no real title available?)
• A Framework for Extended Algebraic Data Types
• A formalization of strong normalization for simply-typed lambda-calculus and System F
• An extension of system \(F\) with subtyping
• Free theorems in the presence of seq
• Guarded recursive datatype constructors
• Intensional polymorphism in type-erasure semantics
• Isabelle/HOL. A proof assistant for higher-order logic
• Meta-programming with built-in type equality
• Parametric polymorphism and operational equivalence
• Programming Languages and Systems
• Syntactic logical relations for polymorphic and recursive types
• Theorem Proving in Higher Order Logics

Cited in

(5)

• A representation theorem for second-order functionals
• scientific article; zbMATH DE number 5033863 (Why is no real title available?)
• Refined typing to localize the impact of forced strictness on free theorems
• Free theorems involving type constructor classes, functional pearl
• Parametricity, type equality, and higher-order polymorphism

Describes a project that uses

Uses Software

• RepLib
• PoplMark
• Isabelle/HOL

This page was built for publication: Free theorems and runtime type representations

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