3 papers
cs.PL2026
Determinacy with Priorities up to Clocks
Luigi Liquori, Michael Mendler, Claude Stolze
In Milner's seminal book on communication and concurrency introducing CCS, a process algebra inherently non-deterministic, chapter 11 was completely devoted to introduce the notion…
cs.LO2020
A Type Checker for a Logical Framework with Union and Intersection Types
Luigi Liquori, Claude Stolze
We present the syntax, semantics, and typing rules of Bull, a prototype theorem prover based on the Delta-Framework, i.e. a fully-typed lambda-calculus decorated with union and int…
cs.LO2018
The Delta-calculus: syntax and types
Luigi Liquori, Claude Stolze
We present the Delta-calculus, an explicitly typed lambda-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different inter…