Semi-Automation of Meta-Theoretic Proofs in Beluga

• Published in: Electronic Proceedings in Theoretical Computer Science
• Main Authors: Schwartzentruber, Johanna, Pientka, Brigitte
• Format: Text
• Language: unknown
• Published: 2023
• Subjects: Computer Science - Programming Languages; Computer Science - Logic in Computer Science; Lambda; Beluga; Beluga*
• Online Access: http://arxiv.org/abs/2311.10439; https://doi.org/10.4204/EPTCS.396.3

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...