ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Tue 13 Sep 2022 10:50 - 11:10 at Linhart - Logic Chair(s): Ilya Sergey

Functional programming language design has been shaped by the framework of natural deduction, in which language constructs are divided into introduction and elimination rules for producers of values. In sequent calculus-based languages, left introduction rules replace (right) elimination rules and provide a dedicated sublanguage for consumers of values. In this paper, we present and analyze a wider design space of programming languages which encompasses four kinds of rules: Introduction and elimination, both left and right. We analyze the influence of rule choice on program structure and argue that having all kinds of rules enriches a programmer’s modularity arsenal. In particular, we identify four ways of adhering to the principle that ''the structure of the program follows the structure of the data`` and show that they correspond to the four possible choices of rules. We also propose the principle of bi-expressibility to guide and validate the design of rules for a connective. Finally, we deepen the well-known dualities between different connectives by means of the proof/refutation duality.

Tue 13 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

10:30 - 12:10
LogicICFP Papers and Events at Linhart
Chair(s): Ilya Sergey National University of Singapore
10:30
20m
Talk
Later Credits: Resourceful Reasoning for the Later Modality
ICFP Papers and Events
Simon Spies MPI-SWS & Saarland University, Lennard Gäher MPI-SWS & Saarland University, Joseph Tassarotti NYU, Ralf Jung MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Lars Birkedal Aarhus University, Derek Dreyer MPI-SWS
DOI
10:50
20m
Talk
Introduction and Elimination, Left and Right
ICFP Papers and Events
Klaus Ostermann University of Tübingen, David Binder University of Tübingen, Ingo Skupin University of Tübingen, Tim Süberkrüb University of Tübingen, Paul Downen University of Massachusetts Lowell
DOI Pre-print
11:10
20m
Talk
Normalization for Fitch-style Modal CalculiDistinguished Paper
ICFP Papers and Events
Nachiappan Valliappan Chalmers University of Technology, Fabian Ruch Unaffiliated, Carlos Tomé Cortiñas Chalmers University of Technology
DOI Media Attached
11:30
20m
Talk
Multiparty GV: Functional Multiparty Session Types With Certified Deadlock Freedom
ICFP Papers and Events
Jules Jacobs Radboud University, Stephanie Balzer Carnegie Mellon University, Robbert Krebbers Radboud University Nijmegen
DOI
11:50
20m
Talk
Back to futuresJFP Presentation
ICFP Papers and Events
Klaas Pruiksma Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA