APLAS 2023
Sun 26 - Wed 29 November 2023 Taipei, Taiwan
Mon 27 Nov 2023 14:00 - 14:30 at Room 106 & 107, IIS - Functional Languages Chair(s): Jihyeok Park

Starting from an encoding of untyped λ-terms with sharing, defined using synthetic inference rules based on a focused proof system for Gentzen’s LJ, we introduce the positive λ-calculus, a call-by-value calculus with explicit substitutions. This calculus is closely related to Accattoli and Paolini’s value substitution calculus but has a different style of reduction rules that provides a good notion of sharing along the reduction. We also propose a graphical representation in order to capture the structural equivalence on terms that can be described using rule permutations. On one hand, this graphical representation provides a way to remove redundancy in the syntax, and on the other hand, it allows implementing basic operations such as substitution and reduction in a straightforward way.

Mon 27 Nov

Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change

13:30 - 15:00
Functional LanguagesAPLAS 2023 at Room 106 & 107, IIS
Chair(s): Jihyeok Park Korea University
13:30
30m
Talk
A Diamond Machine for Strong Evaluation
APLAS 2023
Beniamino Accattoli Inria & Ecole Polytechnique, Pablo Barenbaum Universidad Nacional de Quilmes (CONICET) & Universidad de Buenos Aires
14:00
30m
Talk
Proofs as Terms, Terms as Graphs
APLAS 2023
Jui-Hsuan Wu Institut Polytechnique de Paris
14:30
30m
Talk
Typed Non-determinism in Functional and Concurrent Calculi
APLAS 2023
Bas van den Heuvel University of Groningen, Joseph Paulus , Daniele Nantes-Sobrinho Imperial College London, Jorge A. Pérez University of Groningen