34th Conference on the
Mathematical Foundations of Programming Semantics
MFPS 2018

Important dates

• April 6: paper submission
• April 30: application for student support
• May 11: notification of authors
• May 15: early registration deadline
• May 25: final papers ready
• June 6–9: conference

Invited plenary speakers and special sessions

Special session on differentiable programming

• Keynote lecture:
  Gordon Plotkin (Univ. Edinburgh and Google): A Simple Differential Programming Language
• Marie Kerjean (Univ. Paris 7): A logic of Linear Partial Differential Equations
• Barak Pearlmutter (Maynooth Univ.) Stumbling Blocks on the Road to Differentiable Programming [abstract]

  We are entering a magical era, as everything around us becomes responsive and adaptive. To make this happen, it needs to be easy to make computer programs adapt, and the main road we see ahead is differentiable programming: being able to compute and derivatives (primarily gradients) of arbitrary programs. These differentiation operators should be first class: general, robust, performant, and deeply embedded in compilers. I will discuss some subtle difficulties that arise, which have two main causes: approximation, and use of an explicit basis. Both seem unavoidable when building practical systems, and these issues will only become more prominent as our systems grow in complexity.

• Matthijs Vakar (Univ. Oxford): Diffeological Spaces and Denotational Semantics for Differential Programming

Special session on gradual typing

• Keynote lecture:
  Ronald Garcia (Univ. British Columbia): Gradual Enforcement of Program Invariants
• Joshua Dunfield (Queen's Univ., Ontario): Uncertainty is Hope: logic and gradual typing
• Max New (Northeastern Univ.): Semantic Foundations for Gradual Typing

Special session on quantum programming

• Keynote lecture:
  Neil J. Ross (Dalhousie Univ.): Proto-Quipper: A Circuit Description Language for Quantum Computing [abstract]

  Quipper is a functional programming language for quantum computation which has been used to implement various elaborate quantum algorithms. At the moment, Quipper is implemented as an embedded language, whose host language is Haskell. One of the disadvantages to Quipper being an embedded language is that the Haskell type system, while providing many type-safety properties, is not in general strong enough to ensure the full type-safety of quantum programs.

  The Proto-Quipper language provides a foundation for the development of a stand-alone (i.e., non-embedded) version of Quipper. Like Quipper, Proto-Quipper acts as a circuit description language and provides the ability to treat circuits as data in order to manipulate them as a whole. However, Proto-Quipper is also designed to “enforce the physics”, in the sense that its type system would detect, at compile-time, programming errors that could lead to ill-formed or undefined circuits.

  I will start my talk with a brief introduction to quantum computing and a discussion of the design principles behind Quipper. I will then present Proto-Quipper and discuss open problems.

• Craig Gidney (Google Quantum AI): Optimizing quantum circuits with classical thinking [abstract]

  Although quantum computing is now a decades-old field, there are still many low-hanging opportunities for improving the projected costs of quantum algorithms by orders of magnitude. For example, when designing an efficient quantum algorithm one can often identify nearly-classical subproblems. Efficient classical circuits for these subproblems translate into efficient quantum circuits for the original algorithm.

  This talk will discuss a concrete example of the quantum-to-classical-and-back approach bearing fruit. I will show that preparing a particular type of superposition is equivalent to fitness proportionate selection (a classical task where one has a population of items with associated fitnesses and wishes to sample items with twice as much fitness twice as often). I will then explain an efficient classical algorithm for fitness proportionate selection, and translate it back into the quantum domain to produce the 'subprepare' oracle from arXiv:1805.03662, which prepares (and unprepares) superpositions with hardcoded coefficients 100x more efficiently than previous work.

• Vadym Kliuchnikov (Microsoft Research): Tasks performed by programming languages for quantum computers and how Q# enables them [abstract]

  We will discuss the requirements for programming languages for quantum computers and highlight the differences with programming languages for classical computers. Then we will see how these new requirements are addressed in Q#. This talk will also serve as an introduction to Q#.

• Jennifer Paykin (Univ. Pennsylvania): Preaching to the QWIRE: Verified semantics of quantum circuits [abstract]

  Embedded quantum circuit languages like Quipper, LiQUi|⟩, and ProjectQ let programmers express high-level algorithms using host language libraries and features like recursion and data structures. But how can we verify the correctness of embedded quantum circuits without reasoning about the semantics of the entire host language? QWIRE (pronounced “choir”) is a quantum circuit language embedded in Coq, a dependently-typed programming language and interactive theorem prover. QWIRE both has the benefits of an embedded language and can be formally verified inside Coq itself. In this talk I will present the theory and semantics of QWIRE and show how to formally verify the correctness of quantum programs using QWIRE’s denotational semantics.

• Benoît Valiron (Univ. Paris-Saclay): On Quantum and Classical Control [abstract]

  One perspective on quantum algorithms is that they are classical algorithms having access to a special kind of memory with exotic properties. This perspective suggests that, even in the case of quantum algorithms, the control flow notions of sequencing, conditionals, loops, and recursion are entirely classical. There is however, another notion of control flow, that is itself quantum. The notion of quantum conditional expression is reasonably well-understood: the execution of the two expressions becomes itself a superposition of executions. The quantum counterpart of loops and recursion is however still unclear. In this talk, we argue that, under the right circumstances, a reasonable notion of quantum loops and recursion is possible. To this aim, we first propose a classical, typed, reversible language with lists and fixpoints. We then extend this language to the closed quantum domain (without measurements) by allowing linear combinations of terms and restricting fixpoints to structurally recursive fixpoints whose termination proofs match the proofs of convergence of sequences in infinite-dimensional Hilbert spaces. We additionally give an operational semantics for the quantum language in the spirit of algebraic lambda-calculi.

  The talk will be based on arXiv:1804.00952.

Special session on session types

• Keynote lecture:
  Frank Pfenning (Carnegie Mellon Univ.): Ergometric and Temporal Session Types [abstract]

  [joint work with Ankush Das and Jan Hoffmann]

  We usually analyze sequential programs in terms of time and space complexity. For concurrent programs, there are richer sets of quantities of interest. For example, in fork/join parallelism we analyze work (that is, the total number of operations) and span (that is, time under the assumption of maximal parallelism). Other measures of interest include latency and throughput of pipelines and response times for interactive systems.

  In this talk we show how to extend a system of basic session types for message-passing concurrent processes to capture various aspects of parallel complexity. In particular, we introduce ergometric session types to measure work and temporal session types to measure time. Work and time remain abstract in the sense that we can support different concrete cost models in the same framework. We illustrate our approach via simple examples of message-passing concurrent programs with their types.

  Session types can be viewed as arising from a computational interpretation of linear logic where cut reduction in the sequent calculus corresponds to communication. We provide a preliminary assessment of how well ergometric and temporal types fit with this logical foundation.

• Simon Fowler (Univ. Edinburgh): Session Types without Tiers [abstract]

  Session types statically guarantee that communication complies with a protocol. However, most accounts of session typing do not account for failure, which means they are of limited use in real applications---especially distributed applications---where failure is pervasive.

  We present the first formal integration of asynchronous session types with exception handling in a functional programming language. We define a core calculus which satisfies preservation and progress properties, is deadlock free, confluent, and terminating.

  We provide the first implementation of session types with exception handling for a fully-fledged functional programming language, by extending the Links web programming language; our implementation draws on existing work on algebraic effects and effect handlers.

• Rumyana Neykova (Imperial College): A Session Type Provider: Compile-time Generation of Session Types with Interaction Refinements [abstract]

  Session types is a typing discipline for concurrent and distributed processes that allows errors such as communication mismatches and deadlocks to be detected statically. Refinement types are types elaborated by logical constraints that allow richer and finer-grained specification of application properties, combining types with logical formulae that may refer to program values and can constrain types using arbitrary predicates. Type providers, developed in F#, are compile-time components for on-demand code generation. Their architecture relies on an open-compiler, where provider-authors implement a small interface that allows them to inject new names/types into the programming context as the program is written.

  In this talk, I will present a library that integrates aspects from the above fields to realise practical applications of multiparty refinement session types (MPST) for any .Net language. Our library supports the specification and validation of distributed message passing protocols based on a formulation of asynchronous MPST enriched with interaction refinements: a collection of features related to the refinement of protocols, such as message-type refinements (value constraints) and value dependent control flow. The combination of these aspects—session types for structured interactions, constraint solving from refinement types, and protocol-specific code generation—enables the specification and implementation of enriched protocols in native F# (and any .Net-compiled language) without requiring language extensions or external pre-processing of user programs. A well-typed endpoint program using our library is guaranteed to perform only compliant session I/O actions w.r.t. to the refined protocol, up to premature termination. The safety guarantees are achieved by a combination of static type checking of the generated types for messages and I/O operations, correctness by construction from code generation, and automated inlining of assertions.

• Bernardo Toninho (Universidade Nove de Lisboa): Depending on Session-Typed Processes [abstract]

  Session types are a typing discipline for message-passing concurrency that enables the specification of communication protocols as channel types, which can then be statically and/or dynamically enforced in order to ensure various correctness properties such as deadlock-freedom and protocol compliance.

  However, in most session typing frameworks the language of types (and so, the language of protocols) is kept fairly limited, consisting mainly of sequential descriptions of input and output actions, combined with some form of branching or alternative behaviours.

  In this talk I will present a dependent type theory, realised in a concurrent functional language based on the Curry-Howard interpretation of linear logic, that allows for session processes to depend on functions and vice-versa, as well as for the definition of type-level functions. By enriching the type language in this way, we are able to specify protocols where the choice of the next communication action can truly depend on the specific values of exchanged data -- a significant gain in expressiveness wrt the state of the art. I will also show how the type theoretic nature of the framework allows us to internally describe and prove predicates on process behaviours, akin to dependently-typed specifications of functional programs.

  Finally, in order to both justify some of our design choices and to benchmark the expressiveness of the theory I will introduce a faithful embedding (up-to the theory's internal equality) of the functional layer of the calculus within the session-typed process layer.

Conference program

Click here for the program and for the list of accepted talks. A compact PDF version of the schedule is also available.

Proceedings

The proceedings of MFPS 2018 have been published in Electronic Notes in Theoretical Computer Science, volume 341, December 2018.

Travel to Canada

Most foreign nationals now need an electronic travel authorization before flying to Canada. This applies to all visa-exempt foreign nationals (for example, European citizens). It only costs $7 and can be done efficiently at the eTA website. The eTA requirement does not apply to U.S. citizens, nor to visitors who need an actual visa to travel to Canada.

Registration and local information

Online registration is now closed. You can still register in person at the conference. The registration fees are as follows:

• Regular participants: $110 (MFPS only) or $130 (MFPS and QPL).
• Students: $70 (MFPS only) or $90 (MFPS and QPL).
• Before May 15, there was an early registration discount of $10.

There was a joint MFPS/QPL conference dinner on Wednesday, June 6. The dinner took place at the University Club, 6259 Alumni Crescent (building C440 on the campus map).

For a list of hotels and other accommodation choices, see the Accommodations Page.

For information on how to get to Halifax from the airport, see the Airport Transportation Page.

All MFPS talks were held in room 1009 of the Kenneth C. Rowe Management building at 6100 University Avenue (building E260 on the campus map). The joint QPL/MFPS session was held in room 1020 of the same building. Here is a map of the area:

Student support

Graduate student participation is encouraged at MFPS. Students will pay a reduced registration fee. We will also be able to provide limited support for travel and accommodations to some students. If you are interested in this, please send a request to selinger@mathstat.dal.ca by April 30. Please also arrange for a letter of reference from your supervisor, or appropriate other person, to the same email address, explaining whether the student has access to funding from local sources and how much.

Submissions

Submissions should be prepared using the ENTCS Macros, and should be up to 12 pages long excluding bibliography and appendices. Submissions will be via EasyChair. (The original call for papers, in reference to an older style file, suggested up to 15 pages. Authors may still submit up to 15 pages using the old style file. But they are encouraged to use the latest ENTCS style file, dated 6 March 2018, and up to 12 pages, which is actually more generous because of font and margin differences.)

Committees

Program Committee

• Sam Staton, University of Oxford, UK (chair)
• Marc Bagnol, ENS Lyon, France
• Andrej Bauer, University of Ljubljana, Slovenia
• Dariusz Biernacki, University of Wroclaw, Poland
• Aleš Bizjak, Aarhus University, Denmark
• Valentin Blot, Université Paris-Sud, France
• Steve Brookes, Carnegie Mellon University, USA
• Pierre Clairambault, CNRS and ENS Lyon, France
• Ilias Garnier, Sivienn Inc. and ENS Paris
• Sergey Goncharov, FAU Erlangen-Nürnberg, Germany
• Tobias Heindel, Universität Leipzig, Germany
• Tom Hirschowitz, Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, France
• Patricia Johann, Appalachian State University, USA
• Achim Jung, University of Birmingham, UK
• Ohad Kammar, University of Oxford, UK
• Shin-Ya Katsumata, National Institute of Informatics, Japan
• Catherine Meadows, NRL, USA
• Michael Mislove, Tulane University, USA
• Joel Ouaknine, MPI-SWS, Germany
• Daniela Petrisan, Université Paris Diderot - Paris 7, France
• Azalea Raad, MPI-SWS, Germany
• Tarmo Uustalu, Reykjavik University, Iceland
• Benoît Valiron, LRI - CentraleSupélec, Univ. Paris-Saclay, France
• Valeria Vignudelli, CNRS/ENS Lyon, France
• Noam Zeilberger, University of Birmingham, UK

Steering Committee

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

Local Organizers

• Neil J. Ross
• Peter Selinger

Sponsors

We gratefully acknowledge financial support from:

• U.S. Office of Naval Research (ONR)
• Atlantic Association for Research in the Mathematical Sciences (AARMS)
• Dalhousie University Faculty of Science
• The Pacific Institute for the Mathematical Sciences (PIMS)

Contact

For further information about MFPS 2018, please email sam.staton@cs.ox.ac.uk.