1 citations · 2 across the 6 of their papers we have counts for
Showing 2023Show all
2 papers · 1 filter
cs.PL2023
Contextual Refinement Types
Antoine Gaulin, Brigitte Pientka
We develop an extension of the proof environment Beluga with datasort refinement types and study its impact on mechanized proofs. In particular, we introduce refinement schemas, wh…
cs.PL2023★ 1 cited
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 i…