6 citations · 7 across the 6 of their papers we have counts for
6 papers
Syntax and semantics of focalisation with relative monads and comonads
Éléonore Mangel, Paul-André Melliès, Guillaume Munch-Maccagnoni
The logical principles of focalisation and polarisation can be used to design well-behaved term syntaxes for sequent calculus, which play a role as meta-languages for describing ef…
S4 modal sequent calculus as intermediate logic and intermediate language
Jean Caspar, Guillaume Munch-Maccagnoni
In this short paper, we advocate for the idea that continuation-based intermediate languages correspond to intermediate logics. The goal of intermediate languages is to serve as a…
Linear effects, exceptions, and resource safety: a Curry-Howard correspondence for destructors
Sidney Congard, Guillaume Munch-Maccagnoni, Rémi Douence
We analyse the problem of combining linearity, effects, and exceptions, in abstract models of programming languages, as the issue of providing some kind of strength for a monad $T(…
Classical notions of computation and the Hasegawa-Thielecke theorem (extended version)
Éléonore Mangel, Paul-André Melliès, Guillaume Munch-Maccagnoni
In the spirit of the Curry-Howard correspondence between proofs and programs, we define and study a syntax and semantics for classical logic equipped with a computationally involut…
Resource Polymorphism
Guillaume Munch-Maccagnoni
We present a resource-management model for ML-style programming languages, designed to be compatible with the OCaml philosophy and runtime model. This is a proposal to extend the O…
The duality of computation under focus
Pierre-Louis Curien, Guillaume Munch-Maccagnoni
We review the close relationship between abstract machines for (call-by-name or call-by-value) lambda-calculi (extended with Felleisen's C) and sequent calculus, reintroducing on t…