\(\mathrm{HO}\pi\) in Coq

DOI10.1007/s10817-020-09553-0OpenAlexW3086025821MaRDI QIDQ2031410

Sergueï Lenglet, Guillaume Ambal, Alan Schmitt

Publication date: 9 June 2021

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-020-09553-0

zbMATH Keywords

Coqhigher-order process calculusHowe's method

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• Beluga
• Twelf
• Abella
• PoplMark
• LNgen
• Nominal Isabelle
• GitHub
• Archive Formal Proofs
• metalib

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Characterizing contextual equivalence in calculi with passivation
• Bisimulation for higher-order process calculi
• Mechanizing type environments in weak HOAS
• Nominal techniques in Isabelle/HOL
• A calculus of mobile processes. I
• A linear logical framework
• \(\pi\)-calculus in (Co)inductive-type theory
• Nominal logic, a first order theory of names and binding
• Proving congruence of bisimulation in functional programming languages
• The locally nameless representation
• A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations
• The Theory of Contexts for First Order and Higher Order Abstract Syntax
• Towards a Formally Verified Proof Assistant
• HOCore in Coq
• Formalising the pi-calculus using nominal logic
• de Bruijn notation as a nested datatype
• A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
• Proof-relevant π-calculus: a constructive account of concurrency and causality
• Abella: A System for Reasoning about Relational Specifications
• A case study in programming coinductive proofs: Howe’s method
• A proof theory for generic judgments
• Howe's Method for Contextual Semantics
• Consistency of the theory of contexts
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs
• Higher-order psi-calculi
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• A Distribution Law for CCS and a New Congruence Result for the π-Calculus

This page was built for publication: \(\mathrm{HO}\pi\) in Coq