xOur data center is currently experiencing power issues. Our colleagues are working hard to resolve the issue and keep downtime to a minimum.
ICFP 2021
Sun 22 - Sat 28 August 2021
Mon 23 Aug 2021 02:00 - 02:30 at TyDe - Session III Chair(s): Dominic Orchard

A π-calculus with linear types ensures the privacy and safety of concurrent communication. Allowing shared (unlimited) communication however is key to model real-world services. To implement a decision procedure that type checks a π-calculus process with both linear and shared types one can either rely on user-provided type annotations, or infer the types of the channels created within the process. We choose to reduce the burden on the user by following the latter approach. If we limit ourselves to the shared π-calculus, we can traverse a process bottom-up and eagerly solve typing constraints into substitutions and apply them to the typing context. However, in a setting with both linear and shared types, typing constraints do not always come with a most general solution, and thus cannot always be eagerly solved.

We provide a co-contextual typing inference algorithm that traverses processes bottom-up and, in addition to the typing context, collects a set of typing constraints. We then solve those constraints that have a most general solution (by using well-known unification algorithms) while deferring the rest until more information becomes available. We state clear soundness and completeness theorems separating both these phases, and a progress theorem that ensures that only those constraints without a most general solution are deferred. This work is being mechanised in Agda.

Extended Abstract (paper.pdf)590KiB

Mon 23 Aug

Displayed time zone: Seoul change

01:30 - 03:00
Session IIITyDe at TyDe
Chair(s): Dominic Orchard University of Kent, UK
01:30
30m
Talk
Actions You Can Handle: Dependent Types for AI Plans
TyDe
Alasdair Hill Heriot-Watt University, Ekaterina Komendantskaya Heriot-Watt University, UK, Matthew L. Daggitt Heriot-Watt University, Ronald P. A. Petrick Heriot-Watt University
DOI Pre-print Media Attached
02:00
30m
Talk
Co-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract)
TyDe
Uma Zalakain University of Glasgow, Ornela Dardha University of Glasgow
File Attached