Meta-programming With Built-in Type Equality

DOI10.1016/j.entcs.2007.11.012zbMath1278.68062OpenAlexW2160930653WikidataQ29396391 ScholiaQ29396391MaRDI QIDQ2871838

T. Sheard, Emir Pasalic

Publication date: 10 January 2014

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.11.012

zbMATH Keywords

meta-programmingequality typesmeta-language

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Related Items

Characterizing functions mappable over GADTs, A library for polymorphic dynamic typing, Implicitly heterogeneous multi-stage programming, Type-Safe Code Transformations in Haskell, Free Theorems and Runtime Type Representations

Uses Software

• Coq
• Twelf

Cites Work

• Unnamed Item
• Guarded recursive datatype constructors
• Type-safe cast
• Typing dynamic typing
• Tagless staged interpreters for typed languages
• λν, a calculus of explicit substitutions which preserves strong normalisation
• Fast Decision Procedures Based on Congruence Closure
• A framework for defining logics
• Qualified Types