Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs
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 infer...
Main Authors: | , |
---|---|
Other Authors: | |
Format: | Text |
Language: | English |
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.640.2697 http://www.easychair.org/publications/?page=719614476 |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.640.2697 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.640.2697 2023-05-15T15:41:52+02:00 Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs Nada Habli Amy P. Felty The Pennsylvania State University CiteSeerX Archives http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.640.2697 http://www.easychair.org/publications/?page=719614476 en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.640.2697 http://www.easychair.org/publications/?page=719614476 Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.easychair.org/publications/?page=719614476 text ftciteseerx 2016-01-08T15:55:40Z 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. 1 Text Beluga Beluga* Unknown |
institution |
Open Polar |
collection |
Unknown |
op_collection_id |
ftciteseerx |
language |
English |
description |
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. 1 |
author2 |
The Pennsylvania State University CiteSeerX Archives |
format |
Text |
author |
Nada Habli Amy P. Felty |
spellingShingle |
Nada Habli Amy P. Felty Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs |
author_facet |
Nada Habli Amy P. Felty |
author_sort |
Nada Habli |
title |
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs |
title_short |
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs |
title_full |
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs |
title_fullStr |
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs |
title_full_unstemmed |
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs |
title_sort |
translating higher-order specifications to coq libraries supporting hybrid proofs |
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.640.2697 http://www.easychair.org/publications/?page=719614476 |
genre |
Beluga Beluga* |
genre_facet |
Beluga Beluga* |
op_source |
http://www.easychair.org/publications/?page=719614476 |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.640.2697 http://www.easychair.org/publications/?page=719614476 |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766374747115880448 |