10 citations · 12 across the 6 of their papers we have counts for
4 papers · 1 filter
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…
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.…