Free Theorems and Runtime Type Representations

DOI10.1016/j.entcs.2007.02.043zbMath1316.68043OpenAlexW2131441325MaRDI QIDQ5262947

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

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

Related Items

Parametricity, type equality, and higher-order polymorphism

Uses Software

• Isabelle/HOL
• PoplMark
• RepLib

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An extension of system \(F\) with subtyping
• Isabelle/HOL. A proof assistant for higher-order logic
• Syntactic Logical Relations for Polymorphic and Recursive Types
• Meta-programming With Built-in Type Equality
• Guarded recursive datatype constructors
• A Framework for Extended Algebraic Data Types
• Free theorems in the presence of seq
• Parametric polymorphism and operational equivalence
• Intensional polymorphism in type-erasure semantics
• Theorem Proving in Higher Order Logics
• Programming Languages and Systems