A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
From MaRDI portal
Publication:2802499
DOI10.1007/978-3-662-49498-1_29zbMath1335.68036arXiv1509.03705OpenAlexW2268117882MaRDI QIDQ2802499
Yu-Ting Wang, Gopalan Nadathur
Publication date: 26 April 2016
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1509.03705
Related Items (3)
Fifty Years of Prolog and Beyond ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ Mechanized metatheory revisited
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Formal compiler construction in a logical framework
- Cut-elimination for a logic with definitions and induction
- Isabelle/HOL. A proof assistant for higher-order logic
- Nominal logic, a first order theory of names and binding
- Programming with Higher-Order Logic
- Stratification in Logics of Definitions
- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax
- Pilsner: a compositionally verified compiler for a higher-order imperative language
- Combining Deduction Modulo and Logics of Fixed-Point Definitions
- A framework for defining logics
- Representing Control: a Study of the CPS Transformation
- A proof theory for generic judgments
- Contextual modal type theory
- Formal certification of a compiler back-end or
- CakeML
- A kripke logical relation between ML and assembly
- Theorem Proving in Higher Order Logics
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- A formulation of the simple theory of types
- Programming Languages and Systems
This page was built for publication: A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
