EasyChair Publications
Search
Paper Information
Paper:Nada Habli and Amy Felty
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs
Title:Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs
Authors:Nada Habli and Amy Felty
Keyphrases:coq, hybrid, reasoning framework, syntax translation, higher order abstract syntax
Paper:
Abstract:We describe ongoing work on building an environment to support reasoning in proof assistants that represent formal systems using higher-order abstract syntax (HOAS). We use a simple and general specification language whose syntax supports HOAS. Using this language, we can encode the syntax and inference rules of a variety of formal systems, such as programming languages and logics. We describe our tool, implemented in OCaml, which parses this syntax, and translates it to a Coq library that includes definitions and hints for aiding automated proof in the Hybrid system. Hybrid itself is implemented in Coq, and designed specifically to reason about such formal systems. Given an input specification, the library that is automatically generated by our tool imports the general Hybrid library and adds definitions and hints for aiding automated proof in Hybrid about the specific programming language or logic defined in the specification. This work is part of a larger project to compare reasoning in systems supporting HOAS. Our current work focuses on Hybrid, Abella, Twelf, and Beluga, and the specification language is designed to be general enough to allow the automatic generation of libraries for all of these systems from a single specification.
Volume:Jasmin Christian Blanchette and Josef Urban (editors). PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Series:EPiC Series in Computing
Volume number:14
Pages:67-76
Editors:Jasmin Christian Blanchette and Josef Urban
Page views:16
Downloads:9
BibTeX entry:
@inproceedings{PxTP2013:Translating_Higher-Order_Specifications_to_Coq_Libraries_Supporting_Hybrid_Proofs,
  author    = {Nada Habli and Amy P. Felty},
  title     = {Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs},
  booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EPiC Series in Computing},
  volume    = {14},
  pages     = {67-76},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}