| Dawit Tirore, Jesper Bengtson & Marco Carbone |
A Sound and Complete Projection for Global Types |
Coq |
Paper, Mechanisation |
| Luís Cruz-Filipe, Fabrizio Montesi & Marco Peressotti |
Certifying Choreography Compilation |
Coq |
Paper, Mechanisation |
| Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker & Michael Norrish |
Kalas: A verified, end-to-end compiler for a choreographic language |
HOL4 |
Paper, Mechanisation |
| Joseph Tassarotti, Ralf Jung & Robert Harper |
A higher-order logic for concurrent termination-preserving refinement |
Coq |
Paper, Mechanisation |
| Peter Thiemann |
Intrinsically-typed mechanized semantics for session types |
Agda |
Paper, Mechanisation |
| Matthew Goto, Radha Jagadeesan, Alan Jeffrey, Corin Pitcher & James Riely |
An extensible approach to session polymorphism |
Coq |
Paper, Mechanisation |
| Reynald Affelt & Naoki Kobayashi |
A Coq library for verification of concurrent programs |
Coq |
Paper, Mechanisation |
| Furio Honsell, Marino Miculan & Ivan Scagnetto |
π-calculus in (co)inductive-type theory |
Coq |
Paper, Mechanisation |
| Daniel Hirschkoff |
A full formalisation of π-calculus theory in the calculus of constructions |
Coq |
Paper |
| Tom Melham |
A mechanized theory of the π-calculus in HOL |
HOL |
Paper |
| Otmaine Aït Mohamed |
Mechanizing a π-calculus equivalence in HOL |
HOL |
Paper, Description of mechanisation |
| Christine Röckl & Daniel Hirschkoff |
A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis |
Isabelle/HOL |
Paper |
| Christine Röckl, Daniel Hirschkoff & Stefan Berghofer |
Higher-order abstract syntax with induction in Isabelle/HOL: Formalizing the π-calculus and mechanizing the theory of contexts |
Isabelle/HOL |
Paper |
| Loïc Henry-Gréard |
Proof of the Subject Reduction Property for a Pi-Calculus in Coq |
Coq |
Paper, Mechanisation |
| Andrew D. Gordon & Tom Melham |
Five axioms of alpha-conversion |
HOL |
Paper |
| Simon J. Gay |
A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL |
Isabelle/HOL |
Paper |
| Joëlle Despeyroux |
A Higher-Order Specification of the π-Calculus |
Coq |
Paper |
| Guillaume Gillard |
A Formalization of a Concurrent Object Calculus up to α-Conversion |
Coq |
Paper, Mechanisation |
| Roly Perera & James Cheney |
Proof-relevant π-calculus: a constructive account of concurrency and causality |
Agda |
Paper, Mechanisation |
| Alwen Tiu & Dale Miller |
Proof search specifications of bisimulation and modal logics for the π-calculus |
Abella |
Paper |
| Kaustuv Chaudhuri, Matteo Cimini & Dale Miller |
A Lightweight Formalization of the Metatheory of Bisimulation-Up-To |
Abella |
Paper, Mechanisation |
| Iliano Cervesato, Frank Pfenning, David Walker & Kevin Watkins |
A Concurrent Logical Framework II: Examples and Applications |
CLF |
Paper |
| Jesper Bengtson & Joachim Parrow |
Formalising the pi-calculus using nominal logic |
Isabelle/HOL |
Paper |
| Dominic Orchard & Nobuko Yoshida |
Using session types as an effect system |
Agda |
Paper, Mechanisation |
| Luca Ciccone & Luca Padovani |
A dependently typed linear π-calculus in Agda |
Agda |
Paper, Mechanisation |
| David Castro, Francisco Ferreira & Nobuko Yoshida |
EMTST: Engineering the meta-theory of session types |
Coq |
Paper, Mechanisation |
| Uma Zalakain |
Type-checking session-typed π-calculus with Coq |
Coq |
Paper, Mechanisation |
| Adam Michael Petz |
A Semantics for Attestation Protocols using Session Types in Coq |
Coq |
Paper, Mechanisation |
| Guillaume Ambal, Sergueï Lenglet & Alan Schmitt |
HOπ in Coq |
Coq |
Paper, Mechanisation |
| Peter Brottveit Bock, Agata Murawska, Alessandro Bruni & Carsten Schürmann |
Representing Session Types |
Celf |
Paper (mechanisation in appendix) |
| Hongwei Xi, Zhiqiang Ren, Hanwen Wu & William Blair |
Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus |
ATS |
Paper |
| Andrew K. Hirsch & Deepak Garg |
Pirouette: higher-order typed functional choreographies |
Coq |
Paper, Mechanisation |
| Luís Cruz-Filipe, Fabrizio Montesi & Marco Peressotti |
Formalising a Turing-Complete Choreographic Language in Coq |
Coq |
Paper, Mechanisation |
| Petar Maksimović & Alan Schmitt |
HOCore in Coq |
Coq |
Paper, Mechanisation |
| Joachim Parrow, Johannes Borgström, Palle Raabjerg & Johannes Åman Pohjola |
Higher-order psi-calculi |
Isabelle/HOL |
Paper, Mechanisation |
| Jesper Bengtson, Joachim Parrow & Tjark Weber |
Psi-Calculi in Isabelle |
Isabelle/HOL |
Paper, Mechanisation |
| Temesghen Kahsai & Marino Miculan |
Implementing Spi Calculus Using Nominal Techniques |
Isabelle/HOL |
Paper |
| David Castro-Perez, Francisco Ferreira, Lorenzo Gheri & Nobuko Yoshida |
Zooid: a DSL for certified multiparty computation |
Coq |
Paper, Mechanisation |
| Simon J. Gay, Peter Thiemann & Vasco T. Vasconcelos |
Duality of Session Types: The Final Cut |
Agda |
Paper, Mechanisation |
| Edwin Brady |
Type-driven development of concurrent communicating systems |
Idris |
Paper, Mechanisation |
| Jonas Kastberg Hinrichsen, Jesper Bengtson & Robbert Krebbers |
Actris: session-type based reasoning in separation logic |
Coq |
Paper, Mechanisation |
| Ilya Sergey, James R. Wilcox, and Zachary Tatlock |
Programming and proving with distributed protocols |
Coq |
Paper, Mechanisation |
| Uma Zalakain & Ornela Dardha |
π with leftovers: A mechanisation in Agda |
Agda |
Paper, Mechanisation |
| Christine Röckl |
A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations |
Isabelle/HOL |
Paper |
| Ivan Scagnetto & Marino Miculan |
Ambient Calculus and its Logic in the Calculus of Inductive Constructions |
Coq |
Paper, Mechanisation |
| Johannes Borgström, Shuqin Huang, Magnus Johansson, Palle Raabjerg, Björn Victor, Johannes Åman Pohjola & Joachim Parrow |
Broadcast psi-calculi with an application to wireless protocols |
Isabelle/HOL |
Paper, Mechanisation |
| Jesper Bengtson & Joachim Parrow |
A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle |
Isabelle/HOL |
Paper, Mechanisation |