Operational techniques in PVS -- a preliminary evaluation
From MaRDI portal
Recommendations
- Formal foundations of operational semantics
- More Church-Rosser proofs (in Isabelle/HOL)
- More Church-Rosser proofs (in Isabelle/HOL)
- Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory
- A mechanical proof of the Church-Rosser theorem
Cited in
(9)- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
- PVS\#: streamlined tacticals for PVS
- A PVS theory for term rewriting systems
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem
- More Church-Rosser proofs in \textsc{Beluga}
- Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
- The ESA XMM-Newton science operations centre: making basic space science available to the whole scientific world'
- On generic context lemmas for higher-order calculi with sharing
This page was built for publication: Operational techniques in PVS -- a preliminary evaluation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2703747)
