A higher-order abstract syntax approach to verified transformations on functional programs
From MaRDI portal
Publication:2802499
Abstract: We describe an approach to the verified implementation of transformations on functional programs that exploits the higher-order representation of syntax. In this approach, transformations are specified using the logic of hereditary Harrop formulas. On the one hand, these specifications serve directly as implementations, being programs in the language Lambda Prolog. On the other hand, they can be used as input to the Abella system which allows us to prove properties about them and thereby about the implementations. We argue that this approach is especially effective in realizing transformations that analyze binding structure. We do this by describing concise encodings in Lambda Prolog for transformations like typed closure conversion and code hoisting that are sensitive to such structure and by showing how to prove their correctness using Abella.
Recommendations
- Programming type-safe transformations using higher-order abstract syntax
- Parametric higher-order abstract syntax for mechanized semantics
- Programming type-safe transformations using higher-order abstract syntax
- Functional programming with higher-order abstract syntax and explicit substitutions
- Higher-order Transformations and Type Simulations
Cites work
- scientific article; zbMATH DE number 1696799 (Why is no real title available?)
- scientific article; zbMATH DE number 3291623 (Why is no real title available?)
- scientific article; zbMATH DE number 3400430 (Why is no real title available?)
- scientific article; zbMATH DE number 3410594 (Why is no real title available?)
- A Kripke logical relation between ML and assembly
- A formulation of the simple theory of types
- A framework for defining logics
- A proof theory for generic judgments
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- CakeML
- Combining deduction modulo and logics of fixed-point definitions
- Contextual modal type theory
- Cut-elimination for a logic with definitions and induction
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Formal compiler construction in a logical framework
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle/HOL. A proof assistant for higher-order logic
- Nominal logic, a first order theory of names and binding
- Pilsner: a compositionally verified compiler for a higher-order imperative language
- Programming Languages and Systems
- Programming type-safe transformations using higher-order abstract syntax
- Programming with higher-order logic.
- Representing Control: a Study of the CPS Transformation
- Stratification in logics of definitions
- Theorem Proving in Higher Order Logics
Cited in
(9)- Programming type-safe transformations using higher-order abstract syntax
- Fifty Years of Prolog and Beyond
- Automating the functional correspondence between higher-order evaluators and abstract machines
- scientific article; zbMATH DE number 1615264 (Why is no real title available?)
- scientific article; zbMATH DE number 5033863 (Why is no real title available?)
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Mechanized metatheory revisited
- Higher-order Transformations and Type Simulations
- Programming type-safe transformations using higher-order abstract syntax
This page was built for publication: A higher-order abstract syntax approach to verified transformations on functional programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2802499)
