Mechanizing a Proof by Induction of Process Algebrs Specifications in Higher Order Logic
No abstract available.
Related papers
- Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs ICFP 2024
- A fully adequate shallow embedding of the [pi]-calculus in Isabelle/HOL with mechanized syntax analysis JFP 2003
- Contextual Refinement of Higher-Order Concurrent Probabilistic Programs PLDI 2026
- Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic OOPSLA 2026
- Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection ICFP 2006
- Almost-Sure Termination by Guarded Refinement ICFP 2024
- Recursive proofs for inductive tree data-structures POPL 2012
- The Essence of Higher-Order Concurrent Separation Logic ESOP 2017