The 32nd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXII) will take place on the campus of the Carnegie Mellon University, Pittsburgh, USA, between 23 and 26 May 2016.

MFPS conferences 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.

Invited plenary speakers

• Peter Selinger, Dalhousie, Canada

  Number-theoretic Methods in Quantum Computing (Abstract)

  An important problem in quantum computing is the so-called approximate synthesis problem: to find a circuit, preferably as short as possible, that approximates a given unitary operator up to given ε. For nearly two decades, the standard solution to this problem was the Solovay-Kitaev algorithm, which is based on geometric ideas. This algorithm produces circuits of size 𝓞(log^c(1/ε)), where c is approximately 3.97. It was a long-standing open problem whether the exponent c could be reduced to 1.

  In this talk, I will report on a new class of number-theoretic algorithms that achieve circuit size 𝓞(log(1/ε)), thereby answering the above question positively. In certain important cases, such as the commonly used Clifford+T gate set, one can even find algorithms that are optimal in an absolute sense: the algorithm finds the shortest circuit whatsoever for the given problem instance. This is joint work with Neil J. Ross.

• Brigitte Pientka, McGill, Canada

  Programming Coinductive Proofs Using Observations (Abstract)

  Coinduction is a key proof technique to establish properties about systems that continue to run and produce results (i.e. network or communications protocols, I/O interaction, data streams, or processes) . Yet, mechanizing coinductive proofs about formal systems and representing, generating and manipulating such proofs remains challenging. In this talk, we develop the idea of programming coinductive proofs dual to the idea of programming inductive proofs. Unlike properties about finite data which can be defined by constructing a derivation, properties about infinite data can be described by the possible observations we can make. Dual to pattern matching, a tool for analyzing finite data, we develop the concept of copattern matching, which allows us to describe properties about infinite data. This leads to a symmetric proof language where pattern matching on finite and infinite data can be mixed.

• Steve Brookes, CMU, USA

  A Denotational Approach to Weak Memory Concurrency (Abstract)

  We present a denotational semantics for shared-memory programs, based on a weak memory model. We abandon sequential consistency and traditional trace-based semantic models, which are incapable of representing weak memory behavior such as stale reads and the absence of a total store ordering. Instead our semantic design embodies “true ” concurrency: a program denotes a set of pomsets (partially ordered multi-sets) of actions. Instead of global states, we take a local view of state and work with footprints to detect potential race conditions and keep track of ownership and resources. The combination of footprints with partial order semantics leads to a framework in which we can explore alternatives to sequential consistency. We define a notion of pomset execution that embodies a weak memory model with the following characteristics:

  1. Writes to the same variable appear to happen in the same order, to all threads;
  2. Reads always see the most recently written value;
  3. The atomic operations of each thread happen in program order;
  4. Non-atomic code can be re-ordered in race-free contexts, without affecting execution results.

  These properties are similar to those of the C11 release/acquire memory model underpinning recent logics such as GPS and RSL, so our semantics should be suitable for establishing soundness of, and relationships between, such logics. Our denotational semantic framework offers an alternative to “execution graphs”, commonly used in operational or axiomatic formalizations of weak memory. An execution graph represents the behavior of an entire program, an approach that is inherently non-compositional, and requires the construction of numerous relations (happens-before, reads-from, etc) constrained to satisfy a battery of axioms. Our denotational framework naturally supports compositional (syntax-directed) reasoning.

• Nathalie Bertrand, Inria, France

  Fault diagnosis in probabilistic models (Abstract)

  Fault diagnosis aims at detecting the occurrence of faulty events in partially observable systems, i.e. systems in which not all events are observed. When it comes to probabilistic models, one can relax the notion of diagnosability by requiring that the set of faulty sequences for which no diagnosis can be made is of null measure. In our talk, we will introduce fault diagnosis and explain how to solve the following questions: How to check whether a probabilistic system is diagnosable? And can one control a system so that it is diagnosable? For these diagnosability and active diagnosability problems, as well as for the diagnoser synthesis question, we will establish precise complexity bounds.

Tutorial speakers and special sessions

Important dates

• Submission Deadline: March 3
• Notification: April 8
• Proceedings: May 1
• Conference: May 23-26

Submission information

Submissions should be prepared using the ENTCS Macros, in the form of a PDF file not exceeding 15 pages. Submissions are open on EasyChair.

Local information

The conference will be held at Carnegie Mellon University. Steve Brookes is the local organiser.

Program Committee

• Achim Jung, Birmingham, UK
• Andre Scedrov, UPenn, USA
• Andrej Bauer, Ljubljana, Slovenia
• Andrzej Murawski, Warwick, UK,
• Bart Jacobs, Radboud U, Netherlands
• Bob Coecke, Oxford, UK
• Cameron Freer, Cambridge MA, USA
• Catherine Meadows, NRL , USA
• Catuscia Palamidessi, INRIA, France
• Christine Tasson, PPS Paris, France
• Claudio Russo, MSR Cambridge, UK
• Dusko Pavlovic, Hawaii, US
• Helle Hvid Hansen, TU Delft, Netherlands
• Hugo Herbelin, Paris, France
• Jean Krivine, Paris, France,
• Joel Ouaknine, Oxford, UK
• Lars Birkedal (Chair), Aarhus, Denmark
• Michael Mislove, Tulane, USA
• Neel Krishnaswami, Birmingham, UK
• Paul Blain Levy, Birmingham, UK,
• Peter Dybjer, Chalmers, Sweden
• Prakash Panangaden, Montreal, Canada
• Stefan Milius, Erlangen, Germany
• Steve Brookes, CMU, USA
• Steve Zdancewic, UPenn, USA

Organising Committee

• Achim Jung, Birmingham, UK
• Andrej Bauer, Ljubljana, Slovenia
• Catherine Meadows, NRL, USA
• Joel Ouaknine, Oxford, UK
• Michael Mislove, Tulane, USA
• Prakash Panangaden, Montreal, Canada
• Steve Brookes, CMU, USA