Dr Willem Heijltjes

I'm a Lecturer and Prize Fellow in the Mathematical Foundations group, Department of Computer Science, University of Bath.

My research is in the area of logic and proof theory, and has focused on canonical graphical representations of proof, commonly known as proof nets.


Willem Heijltjes

Publications


Conflict nets: Efficient locally canonical MALL proof nets

Dominic Hughes and Willem Heijltjes

LICS 2016

We give a new notion of proof net for Multiplicative-Additive Linear Logic, that strikes a subtle balance between efficiency and canonicity. Conflict nets are canonical for all local rule commutations, which are those that do not incur a global duplication. As a consequence they have linear size compared to sequent proofs, avoiding the exponential growth of Hughes and Van Glabbeek's Slice Nets.

PDF

screenshot from paper

Proof equivalence in MLL is PSPACE-complete

Willem Heijltjes and Robin Houston

Logical Methods in Computer Science 12(1) 2016

Proof equivalence in MLL with units is shown to be PSPACE-complete, by a reduction from the graphical formalism called Non-Deterministic Constraint Logic. This effectively rules out a satisfactory notion of proof net with units, as such a notion would constitute a tractable decision algorithm for proof equivalence.

PDF | arXiv

screenshot from paper

Proof nets and semi-star-autonomous categories

Willem Heijltjes and Lutz Straßburger

Mathematical Structures in Computer Science 26(5):789-828 (2016)

We consider a notion of semi-star-autonomous category: star-autonomous categories without units, corresponding to Girard's proof nets for MLL. (Available online since November 2014)

PDF | DOI: 10.1017/S0960129514000395

screenshot from paper

Complexity bounds for sum-product logic
via additive proof nets and Petri nets

Willem Heijltjes and Dominic Hughes

LICS 2015

We give an effective correctness criterion for additive proof nets, which is naturally expressed in Petri nets, and is the equivalent of Danos contractibility for MLL. In addition we give simple proof search algorithms for additive linear logic with and without units and an effective correctness algorithm for additive proof nets with units, and we show that first-order additive linear logic is NP-complete.

PDF

screenshot from paper

No proof nets for MLL with units:
Proof equivalence in MLL is PSPACE-complete

Willem Heijltjes and Robin Houston

CSL-LICS 2014

Proof equivalence in MLL with units is shown to be PSPACE-complete, by a reduction from the graphical formalism called Non-Deterministic Constraint Logic. This effectively rules out a satisfactory notion of proof net with units, as such a notion would constitute a tractable decision algorithm for proof equivalence. (Superseded by the journal version Proof equivalence in MLL is PSPACE-complete)

PDF | DOI: 10.1145/2603088.2603126

screenshot from paper

A Proof of Strong Normalisation for the Typed Atomic Lambda-Calculus

Tom Gundersen, Willem Heijltjes, and Michel Parigot

LPAR 2013

The atomic lambda-calculus is a typeable lambda-calculus with explicit sharing, which originates in a Curry-Howard interpretation of a deep-inference system for intuitionistic logic. In this paper we prove strong normalization of the typed atomic lambda-calculus using Tait's reducibility method.

PDF

screenshot from paper

Atomic lambda-calculus:
a typed lambda-calculus with explicit sharing

Tom Gundersen, Willem Heijltjes, and Michel Parigot

LICS 2013

The atomic lambda-calculus is a typeable lambda-calculus with explicit sharing, based on a Curry-Howard-style interpretation of the deep inference proof formalism. Duplication of subterms during reduction proceeds `atomically', i.e. on individual constructors, similar to optimal graph reduction in the style of Lamping. The calculus preserves strong normalisation and achieves fully lazy sharing.

PDF | DOI: 10.1109/LICS.2013.37

screenshot from paper

Proof nets for additive linear logic with units

Willem Heijltjes

LICS 2011

The paper describes canonical proof nets for additive linear logic, or sum-product logic, the internal language of categories with free finite products and co-products. Starting from existing proof nets, which disregard the unit laws, canonical nets are obtained by a simple rewriting algorithm, for which a substantial correctness proof is provided.

Awarded the LICS 2011 Kleene award for best student paper

PDF | DOI: 10.1109/LICS.2011.9

screenshot from paper

Classical Proof Forestry

Willem Heijltjes

Annals of Pure and Applied Logic 161 (11), pp. 1346-1366, 2010

The paper investigates cut-elimination in classical proof forests, a proof formalism for first-order classical logic based on Herbrand's Theorem and backtracking games in the style of Coquand. Cut-free classical proof forests were described by Miller, and are called Expansion Tree Proofs.

Preprint | DOI: 10.1016/j.apal.2010.04.006

screenshot from paper

Workshop papers


Un Lambda-Calcul Atomique

Tom Gundersen, Willem Heijltjes et Michel Parigot

Journées Francophones des Langages Applicatifs 2013

Superseded by Atomic lambda-calculus: a typed lambda-calculus with explicit sharing.

Français | English

screenshot from paper

Proof Forests with Cut Based on Herbrand's Theorem

Willem Heijltjes

Classical Logic & Computation 2008

Superseded by Classical Proof Forestry.

PDF

screenshot from paper

Slides


On MALL proof nets (LL2016, Lyon)

Complexity bounds for sum-product logic

MLL proof equivalence

Atomic lambda-calculus

Proof nets for additive linear logic part 1, part 2

Classical proof forestry

Previously


Postdoctoral researcher

October 2011 - October 2012

Team Parsifal | LIX | École Polytechnique


PhD in Theoretical Computer Science

November 2011 (viva), June 2012 (graduation)

Laboratory for the Foundations of Computer Science (LFCS)
School of Informatics | University of Edinburgh

Doctoral thesis: Graphical Representation of Canonical Proof: Two case studies

Thesis advisor: Professor Alex Simpson


Master of Science in Cognitive Artificial Intelligence

March 2007

Department of Philosophy | Utrecht University

Master's thesis: Graph Rewriting for Natural Deduction and the Proper Treatment of Variables

Winner of the Cognitive Artificial Intelligence thesis award 2007, Department of Philosophy, Utrecht University

Thesis advisors: Professor Albert Visser and Professor Vincent van Oostrom

Contact


Department of Computer Science
1 West 4.67
Claverton Down
Bath
BA2 7AY
United Kingdom
w.b.heijltjes@bath.ac.uk