A higher-order abstract syntax approach to verified transformations on functional programs
From MaRDI portal
Publication:2802499
DOI10.1007/978-3-662-49498-1_29zbMATH Open1335.68036arXiv1509.03705OpenAlexW2268117882MaRDI QIDQ2802499FDOQ2802499
Authors: Yu-Ting Wang, Gopalan Nadathur 
Publication date: 26 April 2016
Published in: Programming Languages and Systems (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1509.03705
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
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Theorem Proving in Higher Order Logics
- Isabelle/HOL. A proof assistant for higher-order logic
- Nominal logic, a first order theory of names and binding
- A framework for defining logics
- Contextual modal type theory
- A formulation of the simple theory of types
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Programming with higher-order logic.
- CakeML
- Title not available (Why is that?)
- Representing Control: a Study of the CPS Transformation
- Cut-elimination for a logic with definitions and induction
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Programming Languages and Systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Kripke logical relation between ML and assembly
- Title not available (Why is that?)
- A proof theory for generic judgments
- Formal compiler construction in a logical framework
- Pilsner: a compositionally verified compiler for a higher-order imperative language
- Stratification in logics of definitions
- Programming type-safe transformations using higher-order abstract syntax
- Combining deduction modulo and logics of fixed-point definitions
Cited In (9)
- Mechanized metatheory revisited
- Automating the functional correspondence between higher-order evaluators and abstract machines
- Title not available (Why is that?)
- Higher-order Transformations and Type Simulations
- Fifty Years of Prolog and Beyond
- Title not available (Why is that?)
- Programming type-safe transformations using higher-order abstract syntax
- Programming type-safe transformations using higher-order abstract syntax
- A Survey of the Proof-Theoretic Foundations of Logic Programming
Uses Software
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)
