Note: this page tends to lag behind the main page. Go there for the latest news.

Various articles

Conference paper

Modular efficient deconstruction with typed pointer reversal

[PDF, February 2024 — HAL.]

Joint work with Jean Caspar, presented at JFLA 2024.

Abstract

Destructors, responsible for releasing memory and other resources in languages such as C++ and Rust, can lead to stack overflows when releasing a recursive structure that is too deep. In certain cases, it is possible to generate an efficient destructor (non-allocating and tail recursive) using a typed variant of pointer reversal. We extend this technique by making it more modular, in order to handle abstract types, separate compilation, and unboxed types.

BibTeX

[CM24] Caspar, J. & Munch-Maccagnoni, G. Modular efficient deconstruction with typed pointer reversal. In JFLA 2024 - 35es Journées Francophones des Langages Applicatifs, pages 1-10, 2024.
@inproceedings{Caspar2024, TITLE = {{Modular efficient deconstruction with typed pointer reversal}}, AUTHOR = {Caspar, Jean and Munch-Maccagnoni, Guillaume}, URL = {https://inria.hal.science/hal-04406342}, BOOKTITLE = {{JFLA 2024 - 35es Journ{\'e}es Francophones des Langages Applicatifs}}, ADDRESS = {Saint-Jacut-de-la-Mer, France}, PAGES = {1-10}, YEAR = {2024}, MONTH = Jan, PDF = {https://inria.hal.science/hal-04406342/file/jfla2024-paper-13.pdf}, HAL_ID = {hal-04406342}, HAL_VERSION = {v1}, }
Draft paper

Boxroot, fast movable GC roots for a better FFI

[PDF, September 2022 — HAL.]

Long version of the work presented at the ML 2022 workshop. Joint work with Gabriel Scherer.

Abstract

We propose a new interface and implementation for managing garbage collector (GC) roots for the OCaml foreign-function interface (FFI), which offers: • better performance than existing root-registration interfaces, • efficient support for multicore OCaml, thanks to a multicore-friendly design, • a reasoning based on resource-management idioms, enabling an easier OCaml FFI in Rust.

BibTeX

[MS22] Munch-Maccagnoni, G. & Scherer, G. Boxroot, fast movable GC roots for a better FFI. In ML Family workshop (ML 2022), 2022.
@TechReport{MunchMaccagnoniScherer2022MLworkshop, author = {Munch-Maccagnoni, Guillaume and Scherer, Gabriel}, date = {2022-09}, institution = {INRIA}, title = {Boxroot, fast movable GC roots for a better FFI}, booktitle = {ML Family workshop (ML 2022)}, creationdate = {2022-11-23T01:39:10}, owner = {gm}, year = {2022}, }
Draft paper

Efficient “out of heap” pointers for multicore OCaml

[PDF, September 2022 — HAL.]

Long version of the work presented at the OCaml 2022 workshop. Artifacts and results for the experiment are fully available on GitLab.

Abstract

This paper reports the good hypothetical performance, in rigorous practical terms, of embedding (borrowing) linearly-allocated values inside garbage-collected values. A companion submission to the ML workshop reports a symmetrical result: how to efficiently embed (own) garbage-collected values inside linearly-allocated values. Taken together, the broader motivation is to show the feasibility of basing linear allocation with re-use (Lafont 1988; Baker 1992) in languages that would still leverage state-of-art garbage collection for non-linear values.

BibTeX

[M22] Munch-Maccagnoni, G. Efficient “out of heap” pointers for multicore OCaml. In OCaml Users and Developers workshop (OCaml 2022), 2022.
@TechReport{munchmaccagnoni2022ocamlworkshop, author = {Munch-Maccagnoni, Guillaume}, date = {2022-09}, institution = {INRIA}, title = {Efficient “out of heap” pointers for multicore OCaml}, booktitle = {OCaml Users and Developers workshop (OCaml 2022)}, creationdate = {2022-11-23T01:39:10}, owner = {gm}, year = {2022}, }
Abstract

Dependent Type Theory in Polarised Sequent Calculus

[PDF, May 2020 — HAL.]

Originally due to be presented at the TYPES 2020 conference (cancelled). Joint work with Étienne Miquey and Xavier Montillet. (Work in progress)

Abstract

We propose to bring together a dependently-typed theory (ECC) and polarised sequent calculus, by presenting a calculus Ldep suitable as a vehicle for compilation and representation of effectful computations. As a first step in that direction, we show that Ldep advantageously factorize a dependently typed continuation-passing style translation for ECC+call/cc. To avoid the inconsistency of type theory with control operators, we restrict their interaction. Nonetheless, in the pure case, we obtain an unrestricted translation from ECC to itself, thus opening the door to the definition of dependently typed compilation transformations.

BibTeX

[M20] Munch-Maccagnoni, G. Dependent Type Theory in Polarised Sequent Calculus (abstract). In TYPES 2020, 2020.
@TechReport{miqueymontilletmunch2020TYPES, author = {Munch-Maccagnoni, Guillaume}, date = {2020-05}, institution = {INRIA}, title = {Dependent Type Theory in Polarised Sequent Calculus (abstract)}, url = {https://hal.inria.fr/hal-02505671}, booktitle = {{TYPES 2020}}, creationdate = {2022-11-23T01:23:38}, hal_id = {hal-02505671}, owner = {gm}, year = {2020}, }
Position paper

Towards better systems programming in OCaml with out-of-heap allocation

[PDF, May 2020 — HAL.]

Presented at the ML 2020 workshop. See also the more recent OCaml 2022 workshop paper.

Abstract

The current multicore OCaml implementation bans so-called “naked pointers”, pointers to outside the OCaml heap unless they follow drastic restrictions. A backwards-incompatible change has been proposed to make way for the new multicore GC in OCaml. I argue that out-of-heap pointers are not an anomaly, but are part of a better systems programming future.

BibTeX

[M20] Munch-Maccagnoni, G. Towards better systems programming in OCaml with out-of-heap allocation. In ML Workshop 2020, pages 1-6, 2020.
@TechReport{munchmaccagnoni2020mlworkshop, author = {Munch-Maccagnoni, Guillaume}, title = {{Towards better systems programming in OCaml with out-of-heap allocation}}, pages = {1-6}, url = {https://hal.inria.fr/hal-03142386}, address = {Jersey City, United States}, booktitle = {{ML Workshop 2020}}, hal_id = {hal-03142386}, hal_version = {v1}, month = Aug, pdf = {https://hal.inria.fr/hal-03142386/file/ml2020-paper8.pdf}, year = {2020}, }
Extended abstract

Efficient Deconstruction with Typed Pointer Reversal

[PDF, July 2019 — HAL.]

Presented at the ML 2019 workshop. Joint work with Rémi Douence. (Work in progress)

Abstract

The resource-management model of C++ and Rust relies on compiler-generated destructors called predictably and reliably. In current implementations, the generated destructor consumes stack space proportionally to the depth of the structure it destructs. We describe a way to derive destructors for algebraic data types that consume a constant amount of stack and heap. We discuss applicability to C++ and Rust, and also some implication for anyone wishing to extend an ML-style language with first-class resources.

BibTeX

[MD19] Munch-Maccagnoni, G. & Douence, R. Efficient Deconstruction with Typed Pointer Reversal (abstract). In ML Family workshop, 2019.
@TechReport{MunchDouence2019, author = {Munch-Maccagnoni, Guillaume and Douence, Rémi}, date = {2019}, title = {Efficient Deconstruction with Typed Pointer Reversal (abstract)}, url = {https://hal.archives-ouvertes.fr/hal-02177326}, booktitle = {ML Family workshop}, owner = {gm}, timestamp = {2020-09-13}, year = {2019}, }
Extended abstract

A resource modality for RAII

[PDF, May 2018 — HAL.]

Presented at the workshop on Syntax and Semantics of Low-Level Languages (LOLA 2018) in Oxford. Joint work with Guillaume Combette. (Work in progress)

Abstract

We model exceptions in a linear, effectful setting by relaxing the notion of monadic strength to contexts that are discardable, in the spirit of C++ destructors. This gives rise to a resource modality reminiscent of unique_ptr and move semantics in C++11. We explore consequences in language design for resource management in functional programming languages.

BibTeX

[CM18] Combette, G. & Munch-Maccagnoni, G. A resource modality for RAII (abstract). In LOLA 2018: Workshop on Syntax and Semantics of Low-Level Languages, 2018.
@TechReport{CombetteMunch2018, author = {Combette, Guillaume and Munch-Maccagnoni, Guillaume}, date = {2018-04-16}, institution = {INRIA}, title = {A resource modality for RAII (abstract)}, url = {https://hal.inria.fr/hal-01806634}, booktitle = {LOLA 2018: Workshop on Syntax and Semantics of Low-Level Languages}, owner = {gm}, timestamp = {2018.04.17}, year = {2018}, }
Manuscript

Resource polymorphism

[PDF, March 2018 — HAL, arXiv.]

Abstract

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 OCaml language with destructors, move semantics, and resource polymorphism, to improve its safety, efficiency, interoperability, and expressiveness. It builds on the ownership-and-borrowing models of systems programming languages (Cyclone, C++11, Rust) and on linear types in functional programming (Linear Lisp, Clean, Alms). It continues a synthesis of resources from systems programming and resources in linear logic initiated by Baker.

It is a combination of many known and some new ideas. On the novel side, it highlights the good mathematical structure of Stroustrup's “Resource acquisition is initialisation” (RAII) idiom for resource management based on destructors, a notion sometimes confused with finalizers, and builds on it a notion of resource polymorphism, inspired by polarisation in proof theory, that mixes C++'s RAII and a tracing garbage collector (GC). In particular, it proposes to identify the types of GCed values with types with trivial destructor: from this definition it deduces a model in which GC is the default allocation mode, and where GCed values can be used without restriction both in owning and borrowing contexts.

The proposal targets a new spot in the design space, with an automatic and predictable resource-management model, at the same time based on lightweight and expressive language abstractions. It is backwards-compatible: current code is expected to run with the same performance, the new abstractions fully combine with the current ones, and it supports a resource-polymorphic extension of libraries. It does so with only a few additions to the runtime, and it integrates with the current GC implementation. It is also compatible with the upcoming multicore extension, and suggests that the Rust model for eliminating data-races applies.

Interesting questions arise for a safe and practical type system, many of which have already been thoroughly investigated in the languages and prototypes Cyclone, Rust, and Alms.

BibTeX

[M18] Munch-Maccagnoni, G. Resource Polymorphism. , 2018.
@TechReport{Munch2018RePo, author = {Munch-Maccagnoni, Guillaume}, title = {Resource Polymorphism}, year = {2018}, date = {2018-01-31}, }
Manuscript

Note on models of polarised intuitionistic logic

[PDF, June 2017 — HAL.]

Abstract

Following renewed interest in duploids arising from the exponential comonad of linear logic (the construction describing polarised intuitionistic translations into linear logic), I summarise here various remarks: • about a decomposition of Girard's “boring” translation as the expression of call-by-value in call-by-name, dual to how thunks are used to express call-by-name in call-by-value • about the coincidence between linear CPS translations and Girard's translations of intuitionistic logic into linear logic, • about a completeness property of historical models of linear logic in the above context • about a rational reconstruction of these translations with the Linear Call-by-Push-Value.

BibTeX

[M17] Munch-Maccagnoni, G. Note on models of polarised intuitionistic logic. , 2017.
@TechReport{Munch-Maccagnoni2017ll-cbpv, author = {Guillaume Munch-Maccagnoni}, title = {Note on models of polarised intuitionistic logic}, year = {2017}, date = {2017-06-16}, url = {https://hal.inria.fr/hal-01540760}, }
Manuscript

Note on Curry's style for Linear Call-by-Push-Value

[PDF, May 2017 — HAL.]

The proof of completeness of focusing (Sections 6.4 to 7) has been presented at the 4th International Workshop on Structures and Deduction (SD 2017), Sep. 2017, Oxford, under the title “What term assignments can do for focusing”.

Abstract

We present Curry-style calculi for intuitionistic (linear) logic with polarised evaluation order and give self-contained proofs of their main properties and of their interpretation into (Linear) Call-by-Push-Value models: subject reduction, confluence, strong normalisation, coherence, soundness, and focusing.

BibTeX

[M17] Munch-Maccagnoni, G. Note on Curry's style for Linear Call-by-Push-Value. , 2017.
[M17] Munch-Maccagnoni, G. What term assignments can do for focusing. In 4th International Workshop on Structures and Deduction (SD 2017), 2017.
@TechReport{Munch-Maccagnoni2017curry, author = {Munch-Maccagnoni, Guillaume}, title = {Note on Curry's style for Linear Call-by-Push-Value}, year = {2017}, date = {2017-05-03}, url = {https://hal.inria.fr/hal-01528857}, } @TechReport{munchmaccagnoni2017SDworkshop, author = {Munch-Maccagnoni, Guillaume}, date = {2017-09}, institution = {INRIA}, title = {What term assignments can do for focusing}, url = {https://hal.inria.fr/hal-01991571}, booktitle = {{4th International Workshop on Structures and Deduction (SD 2017)}}, creationdate = {2022-11-23T01:13:38}, hal_id = {hal-03142386}, owner = {gm}, year = {2017}, }
Conference paper

A Theory of Effects and Resources: Adjunction Models and Polarised Calculi

[PDF, December 2015 — Slides.]

In proc. POPL 2016. Joint work with Marcelo Fiore and Pierre-Louis Curien.

Abstract

We consider the Curry-Howard-Lambek correspondence for effectful computation and resource management, specifically proposing polarised calculi together with presheaf-enriched adjunction models as the starting point for a comprehensive semantic theory relating logical systems, typed calculi, and categorical models in this context.

Our thesis is that the combination of effects and resources should be considered orthogonally. Model theoretically, this leads to an understanding of our categorical models from two complementary perspectives: (i) as a linearisation of CBPV (Call-by-Push-Value) adjunction models, and (ii) as an extension of linear/non-linear adjunction models with an adjoint resolution of computational effects. When the linear structure is cartesian and the resource structure is trivial we recover Levy's notion of CBPV adjunction model, while when the effect structure is trivial we have Benton's linear/non-linear adjunction models. Further instances of our model theory include the dialogue categories with a resource modality of Melliès and Tabareau, and the [E]EC ([Enriched] Effect Calculus) models of Egger, Møgelberg and Simpson. Our development substantiates the approach by providing a lifting theorem of linear models into cartesian ones.

To each of our categorical models we systematically associate a typed term calculus, each of which corresponds to a variant of the sequent calculi LJ (Intuitionistic Logic) or ILL (Intuitionistic Linear Logic). The adjoint resolution of effects corresponds to polarisation whereby, syntactically, types locally determine a strict or lazy evaluation order and, semantically, the associativity of cuts is relaxed. In particular, our results show that polarisation provides a computational interpretation of CBPV in direct style. Further, we characterise depolarised models: those where the cut is associative, and where the evaluation order is unimportant. We explain possible advantages of this style of calculi for the operational semantics of effects.

Keywords

Categorical semantics, Curry-Howard-Lambek correspondence, Intuitionistic logic, Linear logic, Computational effects, Resource modalities, Polarised calculi, Adjunction models.

BibTeX

[CFM16] Curien, P.L., Fiore, M. & Munch-Maccagnoni, G. A Theory of Effects and Resources: Adjunction Models and Polarised Calculi. In Proc. POPL, 2016.
@InProceedings{CFM2016, Title = {{A} {T}heory of {E}ffects and {R}esources: {A}djunction {M}odels and {P}olarised {C}alculi}, Author = {Curien, Pierre-Louis and Fiore, Marcelo and Munch-Maccagnoni, Guillaume}, Booktitle = {Proc. POPL}, Year = {2016}, Doi = {10.1145/2837614.2837652} }
Conference paper

Polarised Intermediate Representation of Lambda Calculus with Sums

[On HALdirect link to PDF.]

In proc. LICS 2015. Joint work with Gabriel Scherer.

Copyright IEEE. Published thanks to the ERC's open access policy.

Abstract

The theory of the λ-calculus with extensional sums is more complex than with only pairs and functions. We propose an untyped representation—an intermediate calculus—for the λ-calculus with sums, based on the following principles:  1) Computation is described as the reduction of pairs of an expression and a context; the context must be represented inside-out,  2) Operations are represented abstractly by their transition rule,  3) Positive and negative expressions are respectively eager and lazy; this polarity is an approximation of the type. We offer an introduction from the ground up to our approach, and we review the benefits.

A structure of alternating phases naturally emerges through the study of normal forms, offering a reconstruction of focusing. Considering further purity assumption, we obtain maximal multi-focusing. As an application, we can deduce a syntax-directed algorithm to decide the equivalence of normal forms in the simply-typed λ-calculus with sums, and justify it with our intermediate calculus.

Keywords

λ-calculus with sums, Intuitionistic logic, Sequent calculus, Abstract machines, Polarization, Focalization, Continuation-passing style, Defunctionalization.

BibTeX

[MS15] Munch-Maccagnoni, G. & Scherer, G. Polarised Intermediate Representation of Lambda Calculus with Sums. In Proceedings of the Thirtieth Annual ACM/IEEE Symposium on Logic In Computer Science (LICS 2015), 2015.
@InProceedings{MunSch2015, Title = {{P}olarised {I}ntermediate {R}epresentation of {L}ambda {C}alculus with {S}ums}, Author = {Munch-Maccagnoni, Guillaume and Scherer, Gabriel}, Booktitle = {Proceedings of the Thirtieth Annual ACM/IEEE Symposium on Logic In Computer Science (LICS 2015)}, Year = {2015}, Doi = {10.1109/LICS.2015.22} }
Conference paper

Formulae-as-Types for an Involutive Negation

[Article with appendicesSlides — July 2014.]

In proc. CSL-LICS 2014.

Adapted from the fourth chapter of my thesis.

Abstract

Negation is not involutive in the λC calculus because it does not distinguish captured stacks from continuations. We show that there is a formulae-as-types correspondence between the involutive negation in proof theory, and a notion of high-level access to the stacks studied by Felleisen and Clements.

We introduce polarised, untyped, calculi compatible with extensionality, for both of classical sequent calculus and classical natural deduction, with connectives for an involutive negation. The involution is due to the ℓ delimited control operator that we introduce, which allows us to implement the idea that captured stacks, unlike continuations, can be inspected. Delimiting control also gives a constructive interpretation to falsity. We describe the isomorphism there is between A and ¬¬A, and thus between ¬∀ and ∃¬.

Keywords

Classical logic, Formulae-as-types, Delimited control operators, Continuations, Polarization, Focalization.

BibTeX

[M14] Munch-Maccagnoni, G. Formulae-as-Types for an Involutive Negation. In Proceedings of the joint meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS), 2014.
@InProceedings{Munch14Involutive, Title = {{F}ormulae-as-{T}ypes for an {I}nvolutive {N}egation}, Author = {Munch-Maccagnoni, Guillaume}, Booktitle = {Proceedings of the joint meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS)}, Year = {2014} }
Conference paper

Models of a Non-Associative Composition

[PDF, December 2013Slides, April 2014.]

In proc. FoSSaCS 2014.

Slightly shortened version of the second chapter of my thesis manuscript.

The original version of this article is available at Springer Link.

Abstract

We characterise the polarised evaluation order through a categorical structure where the hypothesis that composition is associative is relaxed. Duploid is the name of the structure, as a reference to Jean-Louis Loday's duplicial algebras. The main result is a reflection Adj→Dupl where Dupl is a category of duploids and duploid functors, and Adj is the category of adjunctions and pseudo maps of adjunctions. The result suggests that the various biases in denotational semantics: indirect, call-by-value, call-by-name... are a way of hiding the fact that composition is not always associative.

Keywords

Polarization, Call-by-Push-Value, L calculus, direct models, adjunctions.

BibTeX

[M14] Munch-Maccagnoni, G. Models of a Non-Associative Composition. In Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCs), 8412:397-412, Springer Heidelberg, 2014.
@InProceedings{Munch14Duploids, Title = {{M}odels of a {N}on-{A}ssociative {C}omposition}, Author = {Munch-Maccagnoni, Guillaume}, Booktitle = {Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCs)}, Year = {2014}, Editor = {Muscholl, Anca}, Pages = {397--412}, Publisher = {Springer Heidelberg}, Series = {Lecture Notes in Computer Science}, Volume = {8412} }
Conference paper

The duality of computation under focus

[PDF, June 2010.]

In proc. IFIP TCS 2010. Joint work with Pierre-Louis Curien.

The original version is available at www.springerlink.com.

Abstract

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 the way Curien-Herbelin's syntactic kit expressing the duality of computation. We use this kit to provide a term language for a presentation of LK (with conjunction, disjunction, and negation), and to transcribe cut elimination as (non confluent) rewriting. A key slogan here, which may appear here in print for the first time, is that commutative cut elimination rules are explicit substitution propagation rules.

We then describe the focalised proof search discipline (in the classical setting), and narrow down the language and the rewriting rules to a confluent calculus (a variant of the second author's focalising system L). We then define a game of patterns and counterpatterns, leading us to a fully focalised finitary syntax for a synthetic presentation of classical logic, that provides a quotient on (focalised) proofs, abstracting out the order of decomposition of negative connectives.

Keywords

Sequent calculus, classical logic, polarization, focalization, explicit substitutions, pattern matching.

BibTeX

[CM10] Curien, P.L. & Munch-Maccagnoni, G. The duality of computation under focus. In IFIP TCS, 323:165-181, Springer, 2010.
@InProceedings{CurienMunch10, Title = {{T}he duality of computation under focus}, Author = {Curien, Pierre-Louis and Munch-Maccagnoni, Guillaume}, Booktitle = {IFIP TCS}, Year = {2010}, Editor = {Calude, Christian S. and Sassone, Vladimiro}, Pages = {165-181}, Publisher = {Springer}, Series = {IFIP Advances in Information and Communication Technology}, Volume = {323} }
Conference paper

Focalisation and Classical Realisability

[With appendices, PDF.]

In proc. CSL 2009.

Extended version: August 2009. Revised June 2010.

The original version is available at www.springerlink.com.

Abstract

We develop a polarised variant of Curien and Herbelin's lambda-bar-mu-mu-tilde calculus suitable for sequent calculi that admit a focalising cut elimination (i.e. whose proofs are focalised when cut-free), such as Girard's classical logic LC or linear logic. This gives a setting in which Krivine's classical realisability extends naturally (in particular to call-by-value), with a presentation in terms of orthogonality. We give examples of applications to the theory of programming languages.

In this version extended with appendices, we in particular give the two-sided formulation of LC with the involutive classical negation. We also show that there is in classical realisability a notion of internal completeness similar to the one of Ludics.

Keywords

Realizablity, polarisation, focalization, sequent calculus, classical logic, orthogonality, Ludics.

BibTeX

[M09] Munch-Maccagnoni, G. Focalisation and Classical Realisability. In Computer Science Logic '09, 5771:409-423, Springer, Heidelberg, 2009.
@InProceedings{Munch09Foc, Title = {{F}ocalisation and {C}lassical {R}ealisability}, Author = {Munch-Maccagnoni, Guillaume}, Booktitle = {Computer Science Logic '09}, Year = {2009}, Editor = {Erich Gr{\"a}del and Reinhard Kahle}, Pages = {409--423}, Publisher = {Springer, Heidelberg}, Series = {Lecture Notes in Computer Science}, Volume = {5771} }

Other talks (selected)

See above for conference and workshop presentations with a paper available.

PhD thesis

My PhD thesis develops a theory of evaluation order as non-associativity of composition. Here is a reading guide:

  • Chapter I: subsumed by Sections II and III in LICS 2015.
  • Chapter II: published in FoSSaCS 2014.
  • Chapter III: It contains a decomposition of CPS translations where evaluation order choices for delimited control operators are explained with polarities, but the result should be of interest even by ignoring the delimited control parts. It cannot be found elsewhere yet, and will likely appear in several pieces.
  • Chapter IV: earlier and longer version of CSL-LICS 2014, apart from IV.6, some of which is in POPL 2016.

Syntax and Models of a Non-Associative Composition of Programs and Proofs

[PDF: Screen version or Print version.]

Defended December 10th, 2013. Manuscript in English, preceded by an extended abstract in French.

Abstract

The thesis is a contribution to the understanding of the nature, role, and mechanisms of polarisation in programming languages, proof theory and categorical models. Polarisation corresponds to the idea the associativity of composition of morphisms is an hypothesis that has to be relaxed, and underlies many models of computation.

In our demonstration, we introduce duploids, which model polarisation directly. These compositional structures, which, unlike categories, do not always require composition to be associative, are shown to be in correspondence with certain completed forms of categorical adjunctions (Chapter II). This analysis of polarisation is then extended into a fine-grained decomposition of continuation-passing-style (CPS) transformations, which model and implement higher-order programming languages. As an application we show how polarisation accounts for evaluation order in models of delimited control operators (Chapter III). Finally, we give a formulae-as-types interpretation of an involutive negation, which shows the importance of polarisation for constructiveness in proof theory (Chapter IV).

The cornerstone of our approach is an interactive term-based representation of proofs and programs (L calculi) which exposes the structure of polarities. It is based on the correspondence between abstract machines and sequent calculi, and syntheses various trends: the modelling of control, evaluation order and effects in programming languages, the quest for a relationship between categorical duality and continuations, and the interactive notion of construction in proof theory. We give a gentle introduction to our approach which only assumes elementary knowledge of simply-typed λ calculus and rewriting (Chapter I).

Keywords

Non-associative composition, Polarization, Adjunctions, Direct model, Abstract machine, Sequent calculus, Delimited control, Continuation-passing style.

BibTeX

[M13] Munch-Maccagnoni, G. Syntax and Models of a non-Associative Composition of Programs and Proofs. , 2013.
@PhdThesis{Munch13PhD, Title = {{S}yntax and {M}odels of a non-{A}ssociative {C}omposition of {P}rograms and {P}roofs}, Author = {Munch-Maccagnoni, Guillaume}, School = {Univ. Paris Diderot}, Year = {2013} }

Manuscripts & lecture notes

  • Calcul L pour les séquents, April 2012. GdT Logique, February 2012. See also the Chapter I of my PhD thesis. PDF (French)
  • Λ-calcul, machines et orthogonalité, appears in the Chapter I of my PhD thesis (except for the sections about orthogonality-based logical relations which can only be found here at the moment). GdT Logique, October 2011. PDF (French)
    (June 2012: added the proof of strong normalisation by orthogonality, together with a comparison to Krivine's “adapted pairs” technique.)
  • From delimited CPS to polarisation, appears as Chapter III in my PhD thesis. April 2011 (HAL). PDF
  • Étude polarisée du système L, internship report (HAL), 2008: longer and earlier version of Focalisation and Classical Realisability with additional motivations and informal explanations.