Semi-Automation of Meta-Theoretic Proofs in Beluga
We present a sound and complete focusing calculus for the core of the logic behind the proof assistant Beluga as well as an overview of its implementation as a tactic in Beluga's interactive proof environment Harpoon. The focusing calculus is designed to construct uniform proofs over contextual...
Published in: | Electronic Proceedings in Theoretical Computer Science |
---|---|
Main Authors: | , |
Format: | Text |
Language: | unknown |
Published: |
2023
|
Subjects: | |
Online Access: | http://arxiv.org/abs/2311.10439 https://doi.org/10.4204/EPTCS.396.3 |
id |
ftarxivpreprints:oai:arXiv.org:2311.10439 |
---|---|
record_format |
openpolar |
spelling |
ftarxivpreprints:oai:arXiv.org:2311.10439 2023-12-24T10:15:28+01:00 Semi-Automation of Meta-Theoretic Proofs in Beluga Schwartzentruber, Johanna Pientka, Brigitte 2023-11-17 http://arxiv.org/abs/2311.10439 https://doi.org/10.4204/EPTCS.396.3 unknown http://arxiv.org/abs/2311.10439 EPTCS 396, 2023, pp. 20-35 doi:10.4204/EPTCS.396.3 Computer Science - Programming Languages Computer Science - Logic in Computer Science text 2023 ftarxivpreprints https://doi.org/10.4204/EPTCS.396.3 2023-11-26T02:06:50Z We present a sound and complete focusing calculus for the core of the logic behind the proof assistant Beluga as well as an overview of its implementation as a tactic in Beluga's interactive proof environment Harpoon. The focusing calculus is designed to construct uniform proofs over contextual LF and its meta-logic in Beluga: a dependently-typed first-order logic with recursive definitions. The implemented tactic is intended to complete straightforward sub-cases in proofs allowing users to focus only on the interesting aspects of their proofs, leaving tedious simple cases to Beluga's theorem prover. We demonstrate the effectiveness of our work by using the tactic to simplify proving weak-head normalization for the simply-typed lambda-calculus. Comment: In Proceedings LFMTP 2023, arXiv:2311.09918 Text Beluga Beluga* ArXiv.org (Cornell University Library) Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300) Electronic Proceedings in Theoretical Computer Science 396 20 35 |
institution |
Open Polar |
collection |
ArXiv.org (Cornell University Library) |
op_collection_id |
ftarxivpreprints |
language |
unknown |
topic |
Computer Science - Programming Languages Computer Science - Logic in Computer Science |
spellingShingle |
Computer Science - Programming Languages Computer Science - Logic in Computer Science Schwartzentruber, Johanna Pientka, Brigitte Semi-Automation of Meta-Theoretic Proofs in Beluga |
topic_facet |
Computer Science - Programming Languages Computer Science - Logic in Computer Science |
description |
We present a sound and complete focusing calculus for the core of the logic behind the proof assistant Beluga as well as an overview of its implementation as a tactic in Beluga's interactive proof environment Harpoon. The focusing calculus is designed to construct uniform proofs over contextual LF and its meta-logic in Beluga: a dependently-typed first-order logic with recursive definitions. The implemented tactic is intended to complete straightforward sub-cases in proofs allowing users to focus only on the interesting aspects of their proofs, leaving tedious simple cases to Beluga's theorem prover. We demonstrate the effectiveness of our work by using the tactic to simplify proving weak-head normalization for the simply-typed lambda-calculus. Comment: In Proceedings LFMTP 2023, arXiv:2311.09918 |
format |
Text |
author |
Schwartzentruber, Johanna Pientka, Brigitte |
author_facet |
Schwartzentruber, Johanna Pientka, Brigitte |
author_sort |
Schwartzentruber, Johanna |
title |
Semi-Automation of Meta-Theoretic Proofs in Beluga |
title_short |
Semi-Automation of Meta-Theoretic Proofs in Beluga |
title_full |
Semi-Automation of Meta-Theoretic Proofs in Beluga |
title_fullStr |
Semi-Automation of Meta-Theoretic Proofs in Beluga |
title_full_unstemmed |
Semi-Automation of Meta-Theoretic Proofs in Beluga |
title_sort |
semi-automation of meta-theoretic proofs in beluga |
publishDate |
2023 |
url |
http://arxiv.org/abs/2311.10439 https://doi.org/10.4204/EPTCS.396.3 |
long_lat |
ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
geographic |
Lambda |
geographic_facet |
Lambda |
genre |
Beluga Beluga* |
genre_facet |
Beluga Beluga* |
op_relation |
http://arxiv.org/abs/2311.10439 EPTCS 396, 2023, pp. 20-35 doi:10.4204/EPTCS.396.3 |
op_doi |
https://doi.org/10.4204/EPTCS.396.3 |
container_title |
Electronic Proceedings in Theoretical Computer Science |
container_volume |
396 |
container_start_page |
20 |
op_container_end_page |
35 |
_version_ |
1786202372137025536 |