Semi-Automation of Meta-Theoretic Proofs in Beluga

Johanna Schwartzentruber
Brigitte Pientka

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.

In Alberto Ciaffaglione and Carlos Olarte: Proceedings of the 18th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2023), Rome, Italy, 2nd July 2023, Electronic Proceedings in Theoretical Computer Science 396, pp. 20–35.
Published: 17th November 2023.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: