Type-Safe Code Transformations in Haskell

DOI10.1016/j.entcs.2006.10.036zbMath1277.68049OpenAlexW2026691974MaRDI QIDQ2866331

Louis-Julien Guillemette, Stefan Monnier

Publication date: 13 December 2013

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

zbMATH Keywords

compilationtype systemshigher-order abstract syntaxprogram verification

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• Haskell
• TIL
• TALx86

Cites Work

• Unnamed Item
• Unnamed Item
• A syntactic approach to foundational proof-carrying code
• Meta-programming With Built-in Type Equality
• Guarded recursive datatype constructors
• Programming in Ωmega
• Representing Control: a Study of the CPS Transformation
• Type checking with open type functions
• A type system for certified binaries
• Boxes go bananas
• Associated types with class
• Flexible representation analysis
• Formal certification of a compiler back-end or

This page was built for publication: Type-Safe Code Transformations in Haskell