DROPS

Artifact

Software

Intersection Subtyping with Fixpoints

Authors: Olivier Laurent and Jui-Hsuan Wu

Abstract

Cite as

Olivier Laurent, Jui-Hsuan Wu. Intersection Subtyping with Fixpoints (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26938,
   title = {{Intersection Subtyping with Fixpoints}}, 
   author = {Laurent, Olivier and Wu, Jui-Hsuan},
   note = {Software, ANR-21-CE48-0019, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:c8749a7a0cf20e8d37b276595ce0183002fba666;origin=https://github.com/olaure01/islogic;visit=swh:1:snp:d08507fa4c74499420710f1243109b57ad0a4a6d;anchor=swh:1:rev:f0a7d29f8b6c6d3b43d6abb578a6502892600b0e}{\texttt{swh:1:dir:c8749a7a0cf20e8d37b276595ce0183002fba666}} (visited on 2026-07-15)},
   url = {https://github.com/olaure01/islogic/tree/FSCD2026},
   doi = {10.4230/artifacts.26938},
}

Document

DOI: 10.4230/LIPIcs.FSCD.2026.22

Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints

Authors: Olivier Laurent and Jui-Hsuan Wu

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract

Subtyping is a key ingredient of many intersection type systems. In the case of the BCD system, B. Pierce gave a transitivity-free presentation of subtyping. This provides better structural properties for the analysis of this relation and leads to a simple decision algorithm. We generalize this transitivity-free approach to a general class of extensions of BCD allowing to impose some pre-order as well as some fixpoint equations on atoms. This includes in particular the case of various intersection type systems compatible with η-equality (Scott, Park, etc.). Proving the equivalence between the transitivity-free systems and their BCD-style presentation is addressed by means of cut-elimination techniques from proof theory. Due to the presence of fixpoints, we are led to introduce non-wellfounded derivations. In the context of the structural analysis of intersection subtyping, this happens to be the first use of infinitary derivations.

Cite as

Olivier Laurent and Jui-Hsuan Wu. Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{laurent_et_al:LIPIcs.FSCD.2026.22,
  author =	{Laurent, Olivier and Wu, Jui-Hsuan},
  title =	{{Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{22:1--22:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.22},
  URN =		{urn:nbn:de:0030-drops-263721},
  doi =		{10.4230/LIPIcs.FSCD.2026.22},
  annote =	{Keywords: Intersection types, subtyping, non-wellfounded proofs, fixpoints, cut elimination}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.CSL.2023.3

A Positive Perspective on Term Representation (Invited Talk)

Authors: Dale Miller and Jui-Hsuan Wu

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract

We use the focused proof system LJF as a framework for describing term structures and substitution. Since the proof theory of LJF does not pick a canonical polarization for primitive types, two different approaches to term representation arise. When primitive types are given the negative polarity, LJF proofs encode terms as tree-like structures in a familiar fashion. In this situation, cut elimination also yields the familiar notion of substitution. On the other hand, when primitive types are given the positive polarity, LJF proofs yield a structure in which explicit sharing of term structures is possible. Such a representation of terms provides an explicit method for sharing term structures. In this setting, cut elimination yields a different notion of substitution. We illustrate these two approaches to term representation by applying them to the encoding of untyped λ-terms. We also exploit concurrency theory techniques - namely traces and simulation - to compare untyped λ-terms using such different structuring disciplines.

Cite as

Dale Miller and Jui-Hsuan Wu. A Positive Perspective on Term Representation (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{miller_et_al:LIPIcs.CSL.2023.3,
  author =	{Miller, Dale and Wu, Jui-Hsuan},
  title =	{{A Positive Perspective on Term Representation}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{3:1--3:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.3},
  URN =		{urn:nbn:de:0030-drops-174648},
  doi =		{10.4230/LIPIcs.CSL.2023.3},
  annote =	{Keywords: term representation, sharing, focused proof systems}
}

Search Results

Documents authored by Wu, Jui-Hsuan

Intersection Subtyping with Fixpoints

Abstract

Cite as

Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints

Abstract

Cite as

A Positive Perspective on Term Representation (Invited Talk)

Abstract

Cite as

Thanks for your feedback!

Could not send message