HOCore in Coq

DOI10.1007/978-3-319-22102-1_19zbMath1465.68196OpenAlexW2231754610MaRDI QIDQ2945640

Alan Schmitt, Petar Maksimović

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-22102-1_19

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (8)

Trakhtenbrot’s Theorem in Coq ⋮ HOCore in Coq ⋮ Implementation of a reversible distributed calculus ⋮ Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version ⋮ A formal theory of choreographic programming ⋮ Unnamed Item ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ Mechanized metatheory revisited

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• On the expressiveness and decidability of higher-order process calculi
• \(\pi\)-calculus, internal mobility, and agent-passing calculi
• Bisimulation for higher-order process calculi
• Nominal techniques in Isabelle/HOL
• Unique decomposition of processes
• Plain CHOCS. A second generation calculus for higher order processes
• \(\pi\)-calculus in (Co)inductive-type theory
• The locally nameless representation
• A canonical locally named representation of binding
• HOCore in Coq
• Proof search specifications of bisimulation and modal logics for the π-calculus
• Engineering formal metatheory
• A fresh look at programming with names and binders
• Contextual equivalence for higher-order pi-calculus revisited
• Higher-order psi-calculi
• A New Foundation for Nominal Isabelle
• General Bindings and Alpha-Equivalence in Nominal Isabelle
• Psi-calculi in Isabelle
• Foundations of Software Science and Computation Structures

This page was built for publication: HOCore in Coq