with leftovers: a mechanisation in Agda

DOI10.1007/978-3-030-78089-0_9zbMATH Open1490.68143arXiv2005.05902OpenAlexW3177385648MaRDI QIDQ2117018FDOQ2117018

Authors: Uma Zalakain, Ornela Dardha 

Publication date: 21 March 2022

Abstract: Linear type systems need to keep track of how programs use their resources. The standard approach is to use context splits specifying how resources are (disjointly) split across subterms. In this approach, context splits redundantly echo information which is already present within subterms. An alternative approach is to use leftover typing, where in addition to the usual (input) usage context, typing judgments have also an output usage context: the leftovers. In this approach, the leftovers of one typing derivation are fed as input to the next, threading through linear resources while avoiding context splits. We use leftover typing to define a type system for a resource-aware {pi}-calculus, a process algebra used to model concurrent systems. Our type system is parametrised over a set of usage algebras that are general enough to encompass shared types (free to reuse and discard), graded types (use exactly n number of times) and linear types (use exactly once). Linear types are important in the {pi}-calculus: they ensure privacy and safety of communication and avoid race conditions, while graded and shared types allow for more flexible programming. We provide a framing theorem for our type system, generalise the weakening and strengthening theorems to include linear types, and prove subject reduction. Our formalisation is fully mechanised in about 1850 lines of Agda.

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

Recommendations

• scientific article; zbMATH DE number 1104446
• Linearity, session types and the pi calculus
• Resource Usage Analysis for the Pi-Calculus
• Verification, Model Checking, and Abstract Interpretation
• Types for resources in \(\psi\)-calculi

zbMATH Keywords

Agdaconcurrencypi-calculuslinear typesmechanisationleftover typing

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• A calculus of mobile processes. I
• Inductive families
• Title not available (Why is that?)
• The \(\pi\)-calculus: A theory of mobile processes
• Title not available (Why is that?)
• Type systems for concurrent programs.
• Linear type theory for asynchronous session types
• A linear logical framework
• \(\pi\)-calculus in (Co)inductive-type theory
• Formalising the π-Calculus Using Nominal Logic
• Logical relations for fine-grained concurrency
• Lilac: a functional programming language based on linear logic
• Title not available (Why is that?)
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• Session types revisited
• Title not available (Why is that?)
• A Coq library for verification of concurrent programs
• Title not available (Why is that?)
• An extensible approach to session polymorphism
• \textsc{Lincx}: a linear logical framework with first-class contexts
• I got plenty o' nuttin'
• Syntax and semantics of quantitative type theory
• Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic

Cited In (2)

• Non-linear communication via graded modal session types
• Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic

Uses Software

• Lilac
• Agda
• Lincx
• GitHub

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

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