**MFPS XXXVIII (MFPS 2022), Ithaca, NY**
**38th International Conference on Mathematical Foundations of Programming Semantics**
![](assets/cornell-fireworks.jpg)
**MFPS 38 is now over.**
Videos of some of the invited talks and special sessions can be found
[here](https://youtube.com/playlist?list=PLZ7QmqnGR8C03UdduHZ47iBI6BQ3scDfC).
Thank you to all authors, speakers, and attendees!
**MFPS 38** will be held on **July 11-13, 2022**. We plan to hold a hybrid
conference with the in-person event at **Cornell University** in **Ithaca, New
York**, and an in-person local event in Paris, France.
The Ithaca event will be held in room **G01** at the **Bill and Melinda Gates
Hall** on Cornell campus ([map](https://goo.gl/maps/61pdirtQZ8BnJcPB9)).
Additional local information about Ithaca can be found
[here](https://www.cs.cornell.edu/mfps-2022/ithaca.md.html).
The Paris event will take place at
[IRIF](https://www.irif.fr/en/informations/contacts) in **Bâtiment Sophie
Germain**, located at **Pl. Aurélie Nemours, 75013 Paris, France**
([map](https://goo.gl/maps/GNZ7y45a9uqDWzea9)). Additional local information
about the Paris event can be found
[here](https://www.cs.cornell.edu/mfps-2022/paris.md.html).
[MFPS conferences](https://mfpsconf.org/) are dedicated to the areas of
mathematics, logic, and computer science that are related to models of
computation in general, and to semantics of programming languages in particular.
This is a forum where researchers in mathematics and computer science can meet
and exchange ideas. The participation of researchers in neighbouring areas is
strongly encouraged.
Topics include, but are not limited to, the following: bio-computation;
concurrent qualitative and quantitative distributed systems; process calculi;
probabilistic systems; constructive mathematics; domain theory and categorical
models; formal languages; formal methods; game semantics; lambda calculus;
programming-language theory; quantum computation; security; topological models;
logic; type systems; type theory. We also welcome contributions that address
applications of semantics to novel areas such as complex systems, markets, and
networks, for example.
(#) Important Dates
* **Abstract deadline: May 3, 2022**
* Submission deadline: **~~April 29, 2022~~**
- **EXTENDED: May 6, 2022**
* Author notification: **June 10, 2022**
* Pre-proceeding versions: **June 24, 2022**
* Final (post-proceeding) versions: **October 3, 2022**
* Conference dates: **July 11-13, 2022**
All dates are [anywhere on earth](https://time.is/Anywhere_on_Earth).
# Invited Speakers
* [Barbara König](https://www.uni-due.de/theoinf/people/koenig_en.php), University of Duisburg--Essen
Title: Hennessy-Milner Theorems via Galois Connections
Abstract: We introduce a general and compositional, yet simple, framework that
allows us to derive soundness and expressiveness results for modal
logics characterizing behavioural equivalences or metrics (also known as
Hennessy-Milner theorems). It is based on Galois connections between
sets of (real-valued) predicates on the one hand and equivalence
relations/metrics on the other hand and covers a part of the
linear-time-branching-time spectrum, both for the qualitative case
(behavioural equivalences) and the quantitative case (behavioural
metrics). We derive behaviour functions from a given logic and give a
condition, called compatibility, that characterizes under which
conditions a logically induced equivalence/metric is induced by a
fixpoint equation. In particular this framework allows us to derive a
new fixpoint characterization of directed trace metrics.
Joint work with Harsh Beohar, Sebastian Gurke and Karla Messing.
* [Anca Muscholl](https://www.labri.fr/perso/anca/index.html), LaBRI, Université Bordeaux
Title: On Distributed Synthesis
Abstract: Automated synthesis of distributed systems has a big potential since
manually designing such systems is often quite challenging. However, since the
early work of Pnueli and Rosner distributed synthesis acquired the reputation of
being genuinely intractable. Very recently, distributed synthesis with causal
memory was shown by H. Gimbert to be undecidable as well. The talk will present
related results, and show some recent decidability results about the synthesis
of distributed systems that synchronise using locks.
Joint work with H. Gimbert, C. Mascle and I. Walukiewicz.
* [Daniela Petrisan](https://www.irif.fr/~petrisan/), IRIF, Université de Paris
Title: On Weak Distributive Laws in Semantics
Abstract: A unified account of computational effects (such as probabilistic
choice and non-determinism) has been given through the category-theoretic notion
of monad. In this talk we discuss compositionality aspects of such effects when
the corresponding monads cannot be composed via the standard approach based on
distributive laws. We discuss how a weaker notion of distributive laws,
recently considered by Garner, can be used to successfully compose monads such
as the powerset and the finite distributions monads. Finally we show how a weak
distributive law can be regarded as a strong law between slightly modified
monads.
Joint work with Alexandre Goy and Ralph Sarkis.
* [Frank Pfenning](http://www.cs.cmu.edu/~fp/), Carnegie Mellon University
Title: Data Layout from a Type-Theoretic Perspective
Abstract: The specifics of data layout can be important for the efficiency of
functional programs and interaction with external libraries. In this
talk we develop a type-theoretic approach to data layout that could be
used as a typed intermediate language in a compiler or to give a
programmer more control. Our starting point is a computational
interpretation of the semi-axiomatic sequent calculus for intuitionistic
logic that defines abstract notions of cells and addresses. We refine
this semantics so addresses have more structure to reflect possible
alternative layouts without fundamentally departing from intuitionistic
logic. We then add recursive types and explore example programs and
properties of the resulting language.
Joint work with Henry DeYoung.
# Special Sessions
(##) Species of Structures in Algebra, Computation, and Logic
* Organizer: [Marcelo Fiore](https://www.cst.cam.ac.uk/people/mpf23), University of Cambridge
* Organizer: [Nicola Gambino](http://www1.maths.leeds.ac.uk/~pmtng/), University of Leeds
* Speaker: [Martin Hyland](https://www.dpmms.cam.ac.uk/~martin/), University of Cambridge
Title: The Bicategory of Species
Abstract: Generalised species can be understood as the arrows of a
rather special Kleisli bicategory. This perspective places the
Theory of Species within a 2-dimensional structure with many
pleasing features. It provides an interpretation of Linear Logic
analogous to the familiar degenerate Relational Model; and
the differentiation of species parallels the way in which the
Relational Model gives a model for Differential Lambda Calculus.
In a different direction the Theory of Operads finds a natural
expression within the bicategory. Other notions of algebraic
theory can be placed in similar Kleisli bicategories and
one can compare these using some 2-dimensional monad
theory. I shall give an outline of the general theory and of
various connections which it enables. I hope also to convey
some sense of the challenge of creating a clean theory
of structures like the Bicategory of Species.
* Speaker: [André Joyal](https://math.uqam.ca/corps-professoral/professeurs/professeurs-associes/professeur/joyal.andre/), Université du Québec à Montréal
Title: Exponentiable spaces versus coexponentiable algebras
Abstract: Many notions of space happen to be dual to a corresponding notion
of commutative algebra. For example, Stone spaces are dual to Boolean
algebras and locales are dual to frames. The opposite of the category of
topoi has many properties in common with the category of commutative rings
(Anel and Joyal). Dually, the opposite of a category of ring-like structures
often has many properties in common with a category of spaces. For example,
the opposite of the category of commutative rings is the category of affine
schemes. A (presentable) symmetric monoidal closed category becomes a kind of
commutative ring, called a 2-rig, when the colimit operation is viewed as
addition (or totalisation) and the tensor product is viewed as multiplication.
A homomorphism of 2-rigs is defined to be a cocontinuous symmetric monoidal
functor. The category of affine 2-schemes is by definition the opposite of
the category of 2-rigs. The characterisation of exponentiable objects in the
category of affine 2-schemes is open but examples can be constructed in the
context of generalised species (Fiore, Gambino, Hyland and Winskel) and
operads (Gambino and Joyal). The notion of 2-rig has a cartesian version.
The characterisation of exponentiable objects in the corresponding category of
cartesian 2-schemes (= para-topoi) is open but examples can be constructed
from algebraic theories (Fiore and Joyal). I shall review this work and
describe the connection with the theory of polynomial functors.
(##) Relational Verification and Formal Reasoning
* Organizer: [Marco Gaboardi](https://cs-people.bu.edu/gaboardi/), Boston University
* Speaker: [Dave Naumann](https://www.cs.stevens.edu/~naumann/), Stevens Institute of Technology
Title: Towards algebraic foundations for alignment
Abstract: Compositional reasoning about relational properties of programs is
achieved by aligning intermediate points in pairs of program executions, in
order to establish relations at those points. Notions of alignment have
appeared in many guises, often tied to syntactic alignment of program points. A
precise account of alignment is needed to define alignment completeness, which
in turn is needed because the standard logical notion of completeness sheds
little light on relational program logics. In this talk I will review recent
work using Kleene algebra with tests (KAT) to explicate and generalize reasoning
about alignment.
* Speaker: [Hiroshi Unno](http://www.cs.tsukuba.ac.jp/~uhiro/), University of Tsukuba
Title: Constraint-based Relational Verification
Abstract: In recent years they have been numerous works that aim to automate
relational verification. Meanwhile, although Constrained Horn Clauses (CHCs )
empower a wide range of verification techniques and tools, they lack the ability
to express hyperproperties beyond k-safety such as generalized non-interference
and co-termination. This talk describes a novel and fully automated
constraint-based approach to relational verification. We first introduce a new
class of predicate Constraint Satisfaction Problems called pfwCSP where
constraints are represented as clauses modulo first-order theories over
predicate variables of three kinds: ordinary, well-founded, or functional. This
generalization over CHCs permits arbitrary (i.e., possibly non-Horn) clauses,
well-foundedness constraints, functionality constraints, and is capable of
expressing these relational verification problems. Our approach enables us to
express and automatically verify problem instances that require non-trivial
(i.e., non-sequential and non-lock-step) self-composition by automatically
inferring appropriate schedulers (or alignment) that dictate when and which
program copies move. To solve problems in this new language, we present a
constraint solving method for pfwCSP based on stratified CounterExample-Guided
Inductive Synthesis (CEGIS) of ordinary, well-founded, and functional
predicates. We have implemented the proposed framework and obtained promising
results on diverse relational verification problems that are beyond the scope of
the previous verification frameworks.
This is a joint work with Tachio Terauchi (Waseda University) and Eric Koskinen
(Stevens Institute of Technology).
* Speaker: [Francesco Gavazzo](https://sites.google.com/view/francescogavazzo/home), University of Bologna
Title: Relational Theories of Higher-Order Languages: Pure, Effectful, and Coeffectful
Abstract: In this talk, I shall outline recent advances in the development of
relational theories of higher-order sequential programming languages, focusing
on program equivalence and refinement. After having recalled cornerstone results
on the theory of program equivalence for pure languages, I will discuss theories
of program relations for effectful languages, showing how several notions of
effectful program equivalence and refinement can be given in a uniform and
elegant way. I will then move to higher-order languages with combined effects
and coeffects. The addition of coeffectful behaviours makes relational reasoning
challenging, as coeffectful programs naturally ask for finer and more intensonal
notions of equivalence. I will show how general theories of program relations
can be also given for coeffectful languages, provided that we rethink relational
reasoning following a modal and quantitative (substructural) paradigm.
(##) Algebraic Effects
* Organizer: [Ningning Xie](https://xnning.github.io/), University of Cambridge
* Speaker: [Sam Lindley](https://homepages.inf.ed.ac.uk/slindley/), University of Edinburgh
Title: Effect handlers for WebAssembly
Abstract: Effect handlers are a modular and versatile programming abstraction
founded on the theory of algebraic effects. Amongst other things they
provide a uniform mechanism inside the programming language for
defining, customising, and composing a broad range of concurrency
features including actors, async/await, coroutines,
generators/iterators, and lightweight threads. As well as enjoying
considerable research interest, they are actively supported by some of
the main functional programming languages and are central to the
design of several large-scale industrial programming platforms.
WebAssembly is a low-level language and execution environment with a
formal semantics. Originally conceived as a target language for the
web supported by all of the main web browsers, it is now also deployed
more widely, e.g. for content delivery networks, library sandboxing,
and smart contracts. By extending WebAssembly with effect handlers, a
single control abstraction can be provided once and for all. This will
empower compiler engineers to define, customise, and compose a broad
range of concurrency features just by compiling to effect handlers.
I'll present a design for extending WebAssembly with effect
handlers. I'll start at the high-level with a semantics for "sheep"
handlers, a pragmatic synthesis of the two main variants of effect
handlers: shallow handlers and deep handlers. I'll then demonstrate
how to realise "sheep" handlers in a low-level language like
WebAssembly. I'll also illustrate with examples how the effect
handlers abstraction adapts quite naturally to the imperative style
used by many current producers of WebAssembly code.
Joint work with Daniel Hillerström, Daan Leijen, Matija Pretnar,
Andreas Rossberg, and KC Sivamarakrishnan.
* Speaker: [Giorgio Bacci](https://homes.cs.aau.dk/~grbacci/), Aalborg University
Title: Quantitative Algebraic Effects: Sum and Tensor
Abstract: With the emergence of probabilistic programming, which is
characterized by the use of probabilistic nondeterminism as a built-in
computational effect, more emphasis has been put on quantitative reasoning. One
thinks in terms of “how close are two programs?” rather than “are they
completely indistinguishable?”. This concept is best captured by a metric and
was firstly advocated by Giacalone, Jou, and Smolka (1990). To address this
need, Mardare, Panangaden, and Plotkin (2016) proposed a version of equational
reasoning, which they call quantitative equational logic, that captures such
metric reasoning principles and, crucially, characterizes quantitative algebraic
effects, that is algebraic effects on categories of metric spaces. In this talk,
I will review the basic ideas and key results of quantitative equational logic,
and present some more recent results on the composition of its theories via sum
and tensor. During the talk, I will also provide several motivating examples to
offer a pragmatic picture of how the compositional reasoning via sum and tensor
of quantitative equational theories works and how it can be used to deduce
algebraic presentations of nontrivial quantitative algebraic effects in an
almost systematic way.
* Speaker: [Nicolas Wu](https://www.imperial.ac.uk/people/n.wu), Imperial College London
Title: The Scope of Algebraic Effects
Abstract: Algebraic effects offer a versatile framework that covers a wide
variety of effects. However, the family of operations that delimit scopes are
not algebraic and are usually modelled as handlers, thus preventing them from
being used freely in conjunction with algebraic operations. We will discuss a
structured way of handling scoped effects using functorial algebras, which are
both principled and convenient for practical programming.
# Accepted and Conditionally Accepted Papers
* James Laird. Revisiting Decidable Bounded Quantification, via Dinaturality
* Daniele Palombi and Jonathan Sterling. Classifying topoi in synthetic guarded domain theory: The universal property of multi-clock guarded recursion
* Vikraman Choudhury and Marcelo Fiore. Free Commutative Monoids in Homotopy Type Theory
* Alexandre Goy. Weakening and Iterating Laws using String Diagrams
* Ayberk Tosun and Martín Escardó. The Patch Locale of a Spectral Locale in Univalent Type Theory
* Hugo Paquet. Bi-invariance for uniform strategies on event structures
* Chris Barrett, Willem Heijltjes and Guy McCusker. The Functional Machine Calculus
* Tomoya Yoshida. Continuous functions on final comodels of free algebraic theories
* Bart Jacobs. Sufficient Statistics and Split Idempotents in Discrete Probability Theory
* Benedetto Intrigila, Giulio Manzonetto and Nicolas Munnich. Extended Addressing Machines for PCF, with Explicit Substitutions
* Mateusz Pyzik. Call-By-Name Is Just Call-By-Value with Delimited Control
* Jason Z. S. Hu and Brigitte Pientka. A Categorical Normalization Proof for the Modal Lambda-Calculus
* Tao Gu, Robin Piedeleu and Fabio Zanasi. A Complete Diagrammatic Calculus for Boolean Satisfiability
* Takahiro Sanada. Category-Graded Algebraic Theories and Effect Handlers
* Paul-André Melliès and Noam Zeilberger. Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem
* Stefan Zetzsche, Alexandra Silva and Matteo Sammartino. Guarded Kleene Algebra with Tests: Automata Learning
* Masahito Hasegawa. The Internal Operads of Combinatory Algebras
# Conference Program
**This schedule is tentative and may be subject to change.**
Each day will be organized into three sessions:
- **Session 1**: 8:30 AM-10:35 AM EDT, 2:30 PM-4:35 PM CEST, 9:30 PM-11:35 PM JST
- **Session 2**: 11:00 AM-1:00 PM EDT, 5:00 PM-7:00 PM CEST, 12:00 AM-2:00 AM JST (+1)
- **Session 3**: 2:00 PM-3:30 PM EDT, 8:00 PM-9:30 PM CEST, 3:00 AM-4:30 AM JST (+1)
**Times below are EDT (Ithaca).** Add 6 hours for CEST (Paris), add 13 hours for JST (Tokyo).
(##) Monday July 11, 2022
(###) Session 1
- 8:30 AM: Barbara König (**Invited Talk**)
- 9:15 AM: Ayberk Tosun and Martín Escardó. The Patch Locale of a Spectral Locale in Univalent Type Theory
- 9:35 AM: Vikraman Choudhury and Marcelo Fiore. Free Commutative Monoids in Homotopy Type Theory
- 9:55 AM: Masahito Hasegawa. The Internal Operads of Combinatory Algebras
- 10:15 AM: James Laird. Revisiting Decidable Bounded Quantification, via Dinaturality
(###) Special Session: Species of Structures in Algebra, Computation, and Logic
- 11:00 AM: Martin Hyland. The Bicategory of Species
- 12:00 AM: André Joyal. Exponentiable spaces versus coexponentiable algebras
(###) Session 3
- 2:00 PM: Frank Pfenning (**Invited Talk**)
- 2:45 PM: Bart Jacobs. Sufficient Statistics and Split Idempotents in Discrete Probability Theory
- 3:05 PM: Mateusz Pyzik. Call-By-Name Is Just Call-By-Value with Delimited Control
(##) Tuesday July 12, 2022
(###) Session 1
- 8:30 AM: Anca Muscholl (**Invited Talk**)
- 9:15 AM: Paul-André Melliès and Noam Zeilberger. Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem
- 9:35 AM: Stefan Zetzsche, Alexandra Silva and Matteo Sammartino. Guarded Kleene Algebra with Tests: Automata Learning
- 9:55 AM: Tomoya Yoshida. Continuous functions on final comodels of free algebraic theories
- 10:15 AM: Takahiro Sanada. Category-Graded Algebraic Theories and Effect Handlers
(###) Special Session: Algebraic Effects
- 11:00 AM: Sam Lindley. Effect handlers for WebAssembly
- 11:40 AM: Giorgio Bacci. Quantitative Algebraic Effects: Sum and Tensor
- 12:20 PM: Nicolas Wu. The Scope of Algebraic Effects
(###) Session 3
- Open time
(##) Wednesday July 13, 2022
(###) Session 1
- 8:30 AM: Daniela Petrisan (**Invited Talk**)
- 9:15 AM: Alexandre Goy. Weakening and Iterating Laws using String Diagrams
- 9:35 AM: Tao Gu, Robin Piedeleu and Fabio Zanasi. A Complete Diagrammatic Calculus for Boolean Satisfiability
- 9:55 AM: Daniele Palombi and Jonathan Sterling. Classifying topoi in synthetic guarded domain theory: The universal property of multi-clock guarded recursion
- 10:15 AM: Jason Z. S. Hu and Brigitte Pientka. A Categorical Normalization Proof for the Modal Lambda-Calculus
(###) Special Session: Relational Verification and Formal Reasoning
- 11:00 AM: Dave Naumann. Towards algebraic foundations for alignment
- 11:40 AM: Hiroshi Unno. Constraint-based Relational Verification
- 12:20 PM: Francesco Gavazzo. Relational Theories of Higher-Order Languages: Pure, Effectful, and Coeffectful
(###) Session 3
- 2:00 PM: Benedetto Intrigila, Giulio Manzonetto and Nicolas Munnich. Extended Addressing Machines for PCF, with Explicit Substitutions
- 2:20 PM: Hugo Paquet. Bi-invariance for uniform strategies on event structures
- 2:40 PM: Chris Barrett, Willem Heijltjes and Guy McCusker. The Functional Machine Calculus
# Organization
(##) Program Committee
* Sandra Alves, University of Porto
* Arthur Azevedo de Amorim, Boston University
* Lars Birkedal, Aarhus University
* Steve Brookes, Carnegie Mellon University
* Jacques Carette, McMaster University
* Pierre Clairambault, CNRS and Aix-Marseille Université
* Jérémy Dubut, AIST, Tokyo
* Daniel Gratzer, Aarhus University
* Amar Hadzihasanovic, Tallinn University of Technology
* Masahito Hasegawa, Kyoto University
* Favonia, University of Minnesota
* Justin Hsu, Cornell University (co-chair)
* Achim Jung, University of Birmingham
* Delia Kesner, Université Paris-Diderot
* Isabella Mastroeni, Università di Verona
* Michael Mislove, Tulane University
* Renato Neves, Minho University
* Max New, University of Michigan
* Krishna S, IIT Bombay
* Taro Sekiyama, National Institute of Informatics, Tokyo
* Alexandra Silva, Cornell University
* Sam Staton, University of Oxford
* Christine Tasson, Sorbonne Université (co-chair)
* Maaike Zwart, IT University of Copenhagen
(##) Organizing Committee
* Andrej Bauer, University of Ljubljana
* Lars Birkedal, Aarhus University
* Steve Brookes, Carnegie Mellon University
* Justin Hsu, Cornell University
* Achim Jung, University of Birmingham
* Catherine Meadows, Naval Research Laboratory
* Michael Mislove, Tulane University
* Joël Ouaknine, Max Planck Institute for Software Systems
* Prakash Panangaden, McGill University
* Alexandra Silva, Cornell University
* Sam Staton, University of Oxford
* Christine Tasson, Sorbonne Université
(##) Local Organizers
* Dexter Kozen, Cornell University
* Alexandra Silva, Cornell University
# Registration and Accommodations
* The registration link can be found [here][reg]. If you plan to attend MFPS virtually, please use the discount code **`virtual`**. This link also has an option for booking on-campus accommodations: these rooms are townhouse-style, a short walk from the conference location, and $95 per night. The deadline for booking these accommodations is **June 27**.
* If you prefer to stay at a local hotel, we have a room block at the Hilton Canopy downtown that you can book [here][Hilton]. These rooms are only guaranteed to be available until ~~June 10~~ **June 21**. Afterwards, the hotel will accept reservations on a space and rate availability basis.
[reg]: https://event.starrezevents.com/9783521a-dc8d-4adb-a204-8e9a03d4680e/8e0e87f0-ce7a-4061-8821-d0d098569943
[Hilton]: https://www.hilton.com/en/book/reservation/deeplink/?ctyhocn=ITHSSPY&groupCode=MFPS&arrivaldate=2022-07-10&departuredate=2022-07-14&cid=OM,WW,HILTONLINK,EN,DirectLink&fromId=HILTONLINKDIRECT
# Local Event (Paris)
With the generous support of [IRIF](https://www.irif.fr/en/index), we are
planning a local event in Paris, France. The event will run at the same time as
the main MFPS conference on July 11 to July 13, and will take place at
[IRIF](https://www.irif.fr/en/informations/contacts) in **Bâtiment Sophie
Germain**, located at **Pl. Aurélie Nemours, 75013 Paris, France**
([map](https://goo.gl/maps/GNZ7y45a9uqDWzea9)).
For registration and more information about the Paris local event, please see
[here](https://www.cs.cornell.edu/mfps-2022/paris.md.html).
(#) Submission Instructions
Submissions should be made through
[EasyChair](https://easychair.org/conferences/?conf=mfps2022). Papers can be at
most **15 pages** long, excluding bibliography, and should be prepared using the
MFPS macros [here](https://mfpsconf.org/?page_id=309).
(#) Proceedings
A preliminary version will be distributed at the meeting. Final proceedings will
be published in an open-access journal after the meeting.
(#) Code of Conduct
MFPS is organized in cooperation with [ACM SIGLOG](www.siglog.org), and all
participants are expected to observe the ACM [code of
conduct](https://www.acm.org/about-acm/policy-against-harassment).
(#) Contact
For any further information about MFPS 2022, please contact Justin Hsu
() and Christine Tasson ().
(#) Sponsors
![](assets/bowers-cis-logo.png height="100px") ![](assets/irif-logo.png height="100px")
![](assets/siglog-logo.png height="100px")