Programming Type-Safe Transformations Using Higher-Order Abstract Syntax

DOI10.1007/978-3-319-03545-1_16zbMath1426.68061OpenAlexW148278167MaRDI QIDQ2938052

Brigitte Pientka, Olivier Savary-Belanger, Stefan Monnier

Publication date: 13 January 2015

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-03545-1_16

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

Inductive Beluga: Programming Proofs ⋮ LINCX: A Linear Logical Framework with First-Class Contexts ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ Denotational Semantics with Nominal Scott Domains

Uses Software

• Coq
• Beluga
• Haskell
• Twelf
• Freshml
• Abella
• Elf

This page was built for publication: Programming Type-Safe Transformations Using Higher-Order Abstract Syntax