HOCore in Coq

DOI10.1007/978-3-319-22102-1_19MaRDI QIDQ2945640zbMATH OpenOpenAlexFDO

Authors Petar Maksimović, Alan Schmitt

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)

Recommendations

• Formalizing process algebraic verifications in the calculus of constructions
• scientific article; zbMATH DE number 1759486
• scientific article; zbMATH DE number 1082078
• scientific article; zbMATH DE number 1070623
• -calculus in (Co)inductive-type theory

Cites work

• -calculus in (Co)inductive-type theory
• \(\pi\)-calculus, internal mobility, and agent-passing calculi
• A canonical locally named representation of binding
• A fresh look at programming with names and binders
• A new foundation for Nominal Isabelle
• Bisimulation for higher-order process calculi
• Contextual equivalence for higher-order pi-calculus revisited
• Engineering formal metatheory
• Foundations of Software Science and Computation Structures
• General bindings and alpha-equivalence in Nominal Isabelle
• Higher-order psi-calculi
• HOCore in Coq
• scientific article; zbMATH DE number 1082078 (Why is no real title available?)
• scientific article; zbMATH DE number 4196073 (Why is no real title available?)
• Nominal techniques in Isabelle/HOL
• On the expressiveness and decidability of higher-order process calculi
• Plain CHOCS. A second generation calculus for higher order processes
• Proof search specifications of bisimulation and modal logics for the \({\pi}\)-calculus
• Psi-calculi in Isabelle
• The locally nameless representation
• Unique decomposition of processes

Cited in

(11)

• \(\mathrm{HO}\pi\) in Coq
• Mechanized metatheory revisited
• HOCore in Coq
• scientific article; zbMATH DE number 2000441 (Why is no real title available?)
• Trakhtenbrot’s Theorem in Coq
• scientific article; zbMATH DE number 7566073 (Why is no real title available?)
• Importing HOL Light into 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
• Certified implementability of global multiparty protocols

Describes a project that uses

Uses Software

• Coq

This page was built for publication: HOCore in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945640)