Home Page of Luis Caires

The Linear SAM is an abstract machine for mechanically executing session typed programs that precisely correspond to Linear Logic CLL via the propositions-as-types correspondence. The SAM is inspired by a fine-grained analysis of proof conversion and focalisation, and supports a fully deterministic sequential evaluation strategy, which may be implemented via co-routining and session buffered communication. A remarkable feature of the SAM’s design is its ability to seamlessly coordinate sequential session behaviour with concurrent session behaviour within the same program. We provide here a proof-of-concept implementation of the SAM, that suggests its potential to support the native linear execution of general session-functional linear programming languages with concurrency. The more recent distribution is bundled with examples in CLASS source code, including basic session programming, System-F style functional programming, computation on inductive and co-inductive types (naturals, trees, lazy streams), process network programming (e.g. infinite precision process network based binary counter, infinite sieve of Eratosthenes generator)

• The Linear Session Abstract Machine July 2025 (PoC Linear SAM as presented in (2) below, download ZIP JVM CODE + CLASS examples).
  Extension of (2) with recursion, polymorphism and concurrency.
• The Session Abstract Machine Aug 2024 (Artifact for ESOP 24 (2), open source download from Zenodo)

Key Publications

• (1) Luís Caires, Bernardo Toninho. The Linear Session Abstract Machine, August 2024 (journal submission).
• (2) Luís Caires, Bernardo Toninho. The Session Abstract Machine, Programming Languages and Systems – 33rd European Symposium on Programming. ESOP 2024 (2024). Springer-Verlag Lecture Notes in Computer Science 14576 2024.

A proof-of-concept interpreter for CLASS, a linear session-based language. CLASS flexibly supports realistic concurrent programming idioms, while is type system statically ensures that programs never misuse or leak stateful resources or memory, they never deadlock, and they always terminate. The supported language includes efficient pragmatic basic datatypes, ML-style let expressions and primitive operations, but also polymorphism, and recursive and co-recursive types. From version 5.0 up the system also supports light type annotations via type inference. The distribution is bundled with many examples, including:

• basic examples, including those in the papers below
• System-F and processes-as-data style encodings of pure data types
• basic data structures (functional and linked lists, binary trees, queues, …)
• shareable concurrent mutable ADTs (stacks, queues, dictionaries, …)
• resource synchronisation (dining philosophers, barriers, fork-join, sharing ADT wrappers, Hoare-style monitors with conditions, …)

Download source code (from Zenodo) (Java, JavaCC, java.concurrent.util)

Key Publications

• Pedro Rocha, Luís Caires. Safe Session-Based Concurrency with Shared Linear State. Programming Languages and Systems – 32th European Symposium on Programming. ESOP 2023 (2023). Springer-Verlag Lecture Notes in Computer Science 13990.
• CLASS: A Logical Foundation For Typeful Programming With Shared State , Pedro Rocha, PhD thesis, December 2022.
• Pedro Rocha, Luís Caires. Propositions-as-types and Shared State. Proc. ACM Program. Lang. 5. 26th ACM SIGPLAN International Conference on Functional Programming. ICFP 21: 1-30 (2021). Proc. ACM Program. Lang, 5.
• Luís Caires, Jorge A. Pérez. Linearity, Control Effects, and Behavioural Types. Programming Languages and Systems – 26th European Symposium on Programming. ESOP 2017: 229-259. Springer-Verlag Lecture Notes in Computer Science 10201.
• Luís Caires, Frank Pfenning and Bernardo Toninho. Linear Logic Propositions as Session Types. MSCS Mathematical Structures in Computer Science, 26(3): 367-423, Cambridge University Press, 2016.

A type checker for dependent information flow types. DIFT builds on dependent type theory, but, unlike usual dependent types, it crucially allow the security level of a type, rather than just the structural data type itself, to depend on runtime values. Our dependent function and dependent sum information flow types provide a direct, natural and elegant way to express and enforce fine grained security policies on programs, including programs that manipulate structured data types (c.f. DOM objects) in which the security level of a structure element may depend on values dynamically stored in other elements, a challenge to security enforcement in web-based applications. The current type checker implementation (version 1.10), based on the algorithm described in the paper above, is still preliminary, but covers all features of the basic language and type system. It is downloadable as a zip archive, including the main java jar file (the system is written in Scala), the (required) Z3 SMT solver, and sample security lattice definition file.

Key Publications

• Luísa Lourenço, Luís Caires. Dependent Information Flow Types. 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 2015: 317-328.
• Luísa Lourenço, Luís Caires. Information Flow Analysis for Valued-Indexed Data Security Compartments. Trustworthy Global Computing – 8th International Symposium. TGC 2013: 180-198. Springer Verlag Lecture Notes in Computer Science 8358.

The Spatial Logic Model Checker is an automated verification tool that allows the user to verify behavioural and spatial properties of distributed concurrent systems expressed in the pi-calculus of Milner, Parrow and Walker. The algorithm implemented (currently using on-the-fly model-checking techniques) is provably correct for all processes, and complete for the class of bounded processes, an abstract class of processes that includes the finite control fragment of the pi-calculus. The current distribution consists of a single executable, available in OCaml bytecode and native code for both Microsoft Windows and Mac OS X, the source code, a preliminary user’s manual, and a few examples along with their descriptions. It also contains two extensions: SLMC-K an extension of SLMC for security protocol verification based on a variant of the applied pi-calculus of Abadi and Fournet as modelling language, and SLMC-C an extension of SLMC that upports the specification of systems based on Conversation Calculus, a model for dynamic multiparty service-oriented applications.

Key Publications

• Luís Caires, Hugo T. Vieira. SLMC: A Tool for Model Checking Concurrent Systems against Dynamical Spatial Logic Specifications. Tools and Algorithms for the Construction and Analysis of Systems – 18th International Conference. TACAS 2012: 485-491. Springer Verlag Lecture Notes in Computer Science 7214.
• Bernardo Toninho, Luís Caires: A Spatial-Epistemic Logic for Reasoning about Security Protocols. SecCO 2010, Proceedings 8th International Workshop on Security Issues in Concurrency, Electronic Proceedings in Theoretical Computer Science 51, 2010.
• Hugo T. Vieira, L. Caires and J. Seco. The Conversation Calculus: A model of service-oriented computation. European Symposium on Programming ESOP’08, num ber 4960 in Lecture Notes in Computer Science. Springer-Verlag, 2008.
• Luís Caires, Luca Cardelli. A Spatial Logic for Concurrency (Part II). Theoretical Computer Science, Elsevier, 322(3):517-565, 2004.
• Luís Caires. Behavioral and Spatial Properties in a Logic for the Pi-Calculus. Proc. of Foundations of Software Science and Computation Structures FOSSACS’04, num- ber 2987 in Lecture Notes in Computer Science. Springer Verlag, 2004.
• Luís Caires and Luca Cardelli. A Spatial Logic for Concurrency (Part I). Information and Computation, Elsevier, 186(2):194–235, 2003.

Deaf Parrot is a proof-of-concept implementation of a linear type system for shared state programs, based on rely-guarantee protocols, modular, composable, expressive, and automatically verifiable mechanism to control the interference resulting from the interaction of non-local aliases that share access to mutable state.

Online demo available

Key Publications

• Filipe Militão, Jonathan Aldrich, Luís Caires: Composing Interfering Abstract Protocols. 30th European Conference on Object-Oriented Programming. ECOOP 2016: 16:1-16:26. LIPIcs 56.
• Filipe Militão, Rely-Guarantee Protocols for Safe Interference over Shared Memory, PhD thesis, December 2015.
• Filipe Militão, Jonathan Aldrich, Luís Caires. Rely-Guarantee Protocols. Object- Oriented Programming – 28th European Conference. ECOOP 2014: 334-359. Springer Verlag Lecture Notes in Computer Science 8586.
• Filipe Militão, Jonathan Aldrich, Luís Caires: Substructural Typestates. Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification. PLPV