Author name cluster

Aloïs Brunel

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

I&C Journal 2015 Journal Article

Quantitative classical realizability

Aloïs Brunel

Introduced by Dal Lago and Hofmann, quantitative realizability is a technique used to define models for logics based on Multiplicative Linear Logic. A particularity is that functions are interpreted as bounded time computable functions. It has been used to give new and uniform proofs of soundness of several type systems with respect to certain time complexity classes. We propose a reformulation of their ideas in the setting of Krivine's classical realizability. The framework obtained generalizes Dal Lago and Hofmann's realizability, and reveals deep connections between quantitative realizability and a linear variant of Cohen's forcing.

Details DOI

TCS Journal 2015 Journal Article

Realizability models for a linear dependent PCF

Aloïs Brunel
Marco Gaboardi

Recently, Dal Lago and Gaboardi have proposed a type system, named d ℓ PCF as a framework for implicit computational complexity. d ℓ PCF is a non-standard type system for PCF programs which is relatively complete with respect to quantitative properties thanks to the use of linear types inspired by Bounded linear logic and dependent types à la Dependent ML. In this work, we adapt the framework of quantitative realizability and obtain a model for d ℓ PCF. The quantitative realizability model aims at a better understanding of d ℓ PCF type decorations and at giving an abstract semantic proof of intensional soundness.

Details DOI