10 citations · 12 across the 6 of their papers we have counts for
7 papers
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…
Strong Priority and Determinacy in Timed CCS
Luigi Liquori, Michael Mendler
Building on the standard theory of process algebra with priorities, we identify a new scheduling mechanism, called "constructive reduction" which is designed to capture the essence…
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…
A prototype-based approach to object reclassification
Ciaffaglione Alberto, Di Gianantonio Pietro, Honsell Furio +1
We investigate, in the context of functional prototype-based lan- guages, a calculus of objects which might extend themselves upon receiving a message, a capability referred to by…
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…
: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
Furio Honsell, Luigi Liquori, Petar Maksimovic +1
We extend the constructive dependent type theory of the Logical Framework with monadic, dependent type constructors indexed with predicates over judgements, called Lo…
Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks
Furio Honsell, Luigi Liquori, Petar Maksimović +1
We present two extensions of the LF Constructive Type Theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle.…