**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")