\( \pi\) with leftovers: a mechanisation in Agda

DOI10.1007/978-3-030-78089-0_9zbMath1490.68143arXiv2005.05902OpenAlexW3177385648MaRDI QIDQ2117018

Uma Zalakain, Ornela Dardha

Publication date: 21 March 2022

Full work available at URL: https://arxiv.org/abs/2005.05902

zbMATH Keywords

concurrencyAgdapi-calculusmechanisationlinear typesleftover typing

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Lilac
• Agda
• Lincx
• GitHub

Cites Work

• A calculus of mobile processes. I
• Inductive families
• A linear logical framework
• \(\pi\)-calculus in (Co)inductive-type theory
• Session types revisited
• Iris
• A Coq Library for Verification of Concurrent Programs
• Logical relations for fine-grained concurrency
• LINCX: A Linear Logical Framework with First-Class Contexts
• I Got Plenty o’ Nuttin’
• Lilac: a functional programming language based on linear logic
• Syntax and Semantics of Quantitative Type Theory
• Linear type theory for asynchronous session types
• An extensible approach to session polymorphism
• Formalising the π-Calculus Using Nominal Logic
• Formal Methods at the Crossroads. From Panacea to Foundational Support
• Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: \( \pi\) with leftovers: a mechanisation in Agda