\(\pi\)-calculus in (Co)inductive-type theory

DOI10.1016/S0304-3975(00)00095-5zbMath0956.68095MaRDI QIDQ1589654

Marino Miculan, Ivan Scagnetto, Furio Honsell

Publication date: 12 December 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

\(\pi\)-calculushigher-order abstract syntaxlogical frameworksproof checkingtyped \(\pi\)-calculus

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (31)

Executable structural operational semantics in Maude ⋮ Fresh logic: Proof-theory and semantics for FM and nominal techniques ⋮ Variable Binding, Symmetric Monoidal Closed Theories, and Bigraphs ⋮ Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts ⋮ HOCore in Coq ⋮ Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda ⋮ Mechanizing type environments in weak HOAS ⋮ Implementing Spi Calculus Using Nominal Techniques ⋮ ASP\(_{\text{fun}}\) : a typed functional active object calculus ⋮ Psi-calculi in Isabelle ⋮ Psi-calculi in Isabelle ⋮ The representational adequacy of <scp>Hybrid</scp> ⋮ An extensible approach to session polymorphism ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ Proof-relevant π-calculus: a constructive account of concurrency and causality ⋮ Plugging-in proof development environments usingLocksinLF ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Mechanized metatheory revisited ⋮ A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations ⋮ Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types. ⋮ Encoding Generic Judgments ⋮ The Theory of Contexts for First Order and Higher Order Abstract Syntax ⋮ Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic ⋮ Structured coalgebras and minimal HD-automata for the \(\pi\)-calculus ⋮ On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions ⋮ A Framework for Defining Logical Frameworks ⋮ A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle ⋮ A Coq Library for Verification of Concurrent Programs ⋮ Specifying Properties of Concurrent Computations in CLF ⋮ \( \pi\) with leftovers: a mechanisation in Agda ⋮ Two case studies of semantics execution in Maude: CCS and LOTOS

Uses Software

• Coq
• LEGO

Cites Work

• Modal logics for mobile processes
• Using typed lambda calculus to implement formal systems on a machine
• The calculus of constructions
• A calculus of mobile processes. II
• Types for proofs and programs. International workshop TYPES '95, Torino, Italy, June 5--8, 1995. Selected papers
• A theory of bisimulation for the \(\pi\)-calculus
• A natural extension of natural deduction
• A framework for defining logics
• Automating inversion of inductive predicates in Coq
• An application of co-inductive types in Coq: Verification of the alternating bit protocol
• A natural deduction approach to dynamic logic
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: \(\pi\)-calculus in (Co)inductive-type theory