2026-07-23T06:31:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17464 2024-03-06T11:00:02Z ddc:004 open_access

A Positive Perspective on Term Representation (Invited Talk) Miller, Dale Wu, Jui-Hsuan term representation sharing focused proof systems 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dale Miller and Jui-Hsuan Wu 2023 Is Part Of LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2023.3 urn:nbn:de:0030-drops-174648 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.3 eng https://creativecommons.org/licenses/by/4.0/legalcode