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.68036OpenAlexW2268117882MaRDI 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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)
- 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)
