Programming Type-Safe Transformations Using Higher-Order Abstract Syntax

DOI10.1007/978-3-319-03545-1_16zbMATH Open1426.68061OpenAlexW148278167MaRDI QIDQ2938052FDOQ2938052

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)

Cited In (5)

• A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
• Title not available (Why is that?)
• LINCX: A Linear Logical Framework with First-Class Contexts
• Denotational Semantics with Nominal Scott Domains
• Inductive Beluga: Programming Proofs

Uses Software

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

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

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