Search

• < Previous
• 1
• Next >

---

Linear Dependent Types and Relative Completeness

Ugo Dal Lago ; Marco Gaboardi.

A system of linear dependent types for the lambda calculus with full higher-order recursion, called dlPCF, is introduced and proved sound and relatively complete. Completeness holds in a strong sense: dlPCF is not only able to precisely capture the functional behaviour of PCF programs (i.e. how the&nbsp;[&hellip;]

---

Bounded Linear Logic, Revisited

Ugo Dal Lago ; Martin Hofmann.

We present QBAL, an extension of Girard, Scedrov and Scott's bounded linear logic. The main novelty of the system is the possibility of quantifying over resource variables. This generalization makes bounded linear logic considerably more flexible, while preserving soundness and completeness for&nbsp;[&hellip;]

---

On Constructor Rewrite Systems and the Lambda Calculus

Ugo Dal Lago ; Simone Martini.

We prove that orthogonal constructor term rewrite systems and lambda-calculus with weak (i.e., no reduction is allowed under the scope of a lambda-abstraction) call-by-value reduction can simulate each other with a linear overhead. In particular, weak call-by- value beta-reduction can be simulated&nbsp;[&hellip;]

---

(Leftmost-Outermost) Beta Reduction is Invariant, Indeed

Beniamino Accattoli ; Ugo Dal Lago.

Slot and van Emde Boas' weak invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time. Is lambda-calculus a reasonable machine? Is there a way to measure the computational complexity of a lambda-term? This paper presents the first complete&nbsp;[&hellip;]

---

Light Logics and the Call-by-Value Lambda Calculus

Paolo Coppola ; Ugo Dal Lago ; Simona Ronchi Della Rocca.

The so-called light logics have been introduced as logical systems enjoying quite remarkable normalization properties. Designing a type assignment system for pure lambda calculus from these logics, however, is problematic. In this paper we show that shifting from usual call-by-name to call-by-value&nbsp;[&hellip;]

---

On the Termination Problem for Probabilistic Higher-Order Recursive Programs

Naoki Kobayashi ; Ugo Dal Lago ; Charles Grellois.

In the last two decades, there has been much progress on model checking of both probabilistic systems and higher-order programs. In spite of the emergence of higher-order probabilistic programming languages, not much has been done to combine those two approaches. In this paper, we initiate a study&nbsp;[&hellip;]

---

On Higher-Order Probabilistic Subrecursion

Flavien Breuvart ; Ugo Dal Lago ; Agathe Herrou.

We study the expressive power of subrecursive probabilistic higher-order calculi. More specifically, we show that endowing a very expressive deterministic calculus like G\"odel's $\mathbb{T}$ with various forms of probabilistic choice operators may result in calculi which are not equivalent as for&nbsp;[&hellip;]

---