6-9 Jun 2012
Bath, England
MFPS XXVIII
http://www.math.tulane.edu/~mfps/MFPS28
Twenty-eighth Conference on the
Mathematical Foundations of
Programming Semantics
University of Bath
United Kingdom
6 - 9 June 2012
For a preliminary PROGRAMME scroll down to the end of this email
For CONFERENCE REGISTRATION and HOTEL RESERVATION follow the links
given at http://www.math.tulane.edu/~mfps/MFPS28
The Twenty-eighth Conference on the Mathematical Foundations of
Programming Semantics will take place on the campus of the
University of Bath, United Kingdom from June 6 through June 9, 2012.
MFPS conferences are devoted to those areas of mathematics, logic,
and computer science that are related to models of computation, in
general, and to the semantics of programming languages, in
particular. The series has particularly stressed providing a forum
where researchers in mathematics and computer science can meet and
exchange ideas about problems of common interest. As the series also
strives to maintain breadth in its scope, the conference strongly
encourages participation by researchers in neighbouring areas.
TOPICS include, but are not limited to, the following: biocomputation;
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 SPEAKERS:
Steve Awodey, CMU
Michael Clarkson, GWU
Patricia Johann, Strathclyde
Dexter Kozen, Cornell
Drew Moshier, Chapman
John Power, Bath
SPECIAL SESSIONS: There will be three special sessions at the meeting,
each associated with one of the plenary talks:
* Logic, computation and algebraic topology,
organised by Steve Awodey and Michael Mislove
* Computational effects, organised by John Power
* Computability on Continuous Data, organised by Drew Moshier
This session is in association with the Alan Turing Centenary
TUTORIALS: There also will be a series of Tutorial Lectures on Game
Semantics. These are being organized by Andrea Schalk (Manchester) and
Paul-Andre Mllies (Paris VII), The speakers will include the
organizers as well as Martin Hyland (Cambridge) and Luke Ong (Oxford).
PROGRAM COMMITTEE:
Thorsten Altenkirch, U Nottingham, UK
Steve Awodey, Carnegie Mellon U, USA
Andrej Bauer, U Ljubljana, Slovenia
Ulrich Berger, Swansea U, UK (Chair)
Stephen Brookes, Carnegie Mellon U, USA
Bob Coecke, U Oxford, UK
Martin Escardo, U Birmingham, UK
Marcelo Fiore, U Cambridge, UK
Neil Ghani, U Strathclyde, UK
Alexey Gotsman, IMDEA, Madrid, Spain
Hugo Herbelin, INRIA, Rocquencourt-Paris, France
Achim Jung, U Birmingham, UK
Daniel Leivant, U Indiana, USA
Guy McCusker, U Bath, UK
Catherine Meadows, NRL, USA
Michael Mislove, Tulane U, USA
Peter O'Hearn, Queen Mary U London, UK
Luke Ong, U Oxford, UK
Prakash Panangaden, McGill U, Canada
John Power, U Bath, UK
Jan Rutten, Radboud Nijmegen, Netherlands
Alex Simpson, U Edinburgh, UK
James Worrell, U Oxford, UK
PROCEEDINGS: There will be a preliminary proceedings of the
conference papers that will be distributed at the meeting, with a
final proceedings published in ENTCS after the meeting.
The Organisers of the MFPS series are Stephen Brookes (CMU),
Achim Jung (Birmingham), Catherine Meadows (NRL),
Michael Mislove (Tulane) and Prakash Panangaden (McGill).
The local arrangements for MFPS XXVIII are being overseen
by Guy McCusker (Bath) and John Power (Bath).
PRELIMINARY PROGRAMME
Wednesday June 6
8:30-9:30 Tutorial 1 on Game Semantics
Andrea Schalk, Manchester
Introduction to game semantics
9:30-9:50 Break
9:50-10:50 Plenary Address
Patricia Johann, Strathclyde
Lifting Functors: Induction, Coinduction, and (maybe) Parametricity
10:50-11:00 Break
11:00-11:30
Stephen Brookes
Concurrent Separation Logic and Syntactic Control of Interference
11:30-12:00
Aquinas Hobor and Robert Dockins
Time Bounds for General Function Pointers
12:00-13:30 Lunch
Session on Logic, computation and algebraic topology
13:30-14:30 Plenary Address
Steve Awodey, CMU
Homotopy Type Theory
14:30-15:00
Sanjeevi Krishnan
Title tba
15:00-15:20 Break
15:20-15:50
Eric Goubault
Geometry of trace spaces and (some) applications
15:50-16:20
Nicola Gambino
Homotopy-initial W-types
16:20-16:50
Andrej Bauer
Automation of proofs in HoTT
End of session on Logic, computation and algebraic topology
16:50-17:00 Break
17:00-17:30
Joachim Kock
Data Types with Symmetries and Polynomial Functors Over Groupoids
17:30-18:00
Naohiko Hoshino
A Representation Theorem for Unique Decomposition Categories
19:00 Reception at the Roman Baths
Thursday, 7 June
8:30-9:30 Tutorial 2 on Game Semantics
Paul-Andre Mellies, Paris VII
Tensorial logic, dialogue categories and games
9:30-9:50 Break
9:50-10:50 Plenary Address
Michael Clarkson, GWU
Mathematical Foundations for Computer Security
10:50-11:00 Break
11:00-11:30
Matteo Cimini, Mohammadreza Mousavi, Michel Reniers
and Murdoch Gabbay
Nominal SOS
11:30-12:00
Murdoch Gabbay and Dan Ghica
Game Semantics in the Nominal Model
12:00-13:30 Lunch
Session on Computational effects
13:30-14:30 Plenary Address
John Power, Bath
Category Theoretic Understandings of Universal Algebra and
its dual: monads and Lawvere theories, comonads and ?
14:30-15:00
Alex Simpson
Observational equivalence for computational effects
15:00-15:20 Break
15:20-15:50
Neil Ghani
Fibrational Induction Meets Effects
15:50-16:20
Andrej Bauer
A semantic account of an effect system
16:20-16:50
Sam Staton
State-passing style
End of Session on Computational effects
16:50-17:00 Break
17:00-17:30
Ingo Battenfeld
Observationally-induced effects in cartesian closed categories
17:30-18:00
Barbara Petit
Continuation Models for the Lambda Calculus with Constructors
Friday, 8 June
8:30-9:30 Tutorial 3 on Game Semantics
Martin Hyland, Cambridge
9:30-9:50 Break
9:50-10:20
Ugo Montanari and Matteo Sammartino
Network Conscious pi-calculus: a Concurrent Semantics
10:20-10:50
Toby Wilkinson
A Characterisation of Expressivity for Coalgebraic Bisimulation
and Simulation
10:50-11:00 Break
11:00-11:30
Filippo Bonchi, Marcello Bonsangue, Georgiana Caltais, Jan Rutten
and Alexandra Silva
Final Semantics for Decorated Traces
11:30-12:00
Dan Teodosiu
A Truly Concurrent Process Semantics over Multi-Pomsets
of Consumable Resources
12:00-13:30 Lunch
Session on Computability on Continuous Data
This session is part of the ATY
13:30-14:30 Plenary Address
Drew Moshier
Title tba
14:30-15:00
Nick Bezhanishili
Logics for compact Hausdorff spaces
15:00-15:20 Break
15:20-15:50
Paul Taylor
Semilattice bases for locally compact spaces
15:50-16:20
Jens Blanck
Interval domains and computable sequences
16:20-16:50
Martin Escardo
The intrinsic topology of a Martin-Lof universe, with an application to
Rice's theorem for the universe
End of Session on Computability on Continuous Data
16:50-17:00 Break
17:00-17:30
Oleksandr Manzyuk
A Simply Typed Lambda-Calculus of Forward Automatic Differentiation
17:30-18:00
Andrew Lawrence, Ulrich Berger and Monika Seisenberger
Extracting a DPLL Algorithm
20:00 Dinner at the Roman Baths
Saturday, 9 June
8:30-9:30 Tutorial 4 on Game Semantics
Luke Ong, Oxford
Two-level Game Semantics, Intersection Types and
Higher-Order Model Checking
13:00-9:50 Break
9:50-10:20
Dan Ghica and Nikos Tzevelekos
A System-Level Game Semantics
10:20-10:50
Guy McCusker, John Power and Cai Wingfield.
A Graphical Foundation for Schedules
10:50-11:00 Break
11:00-11:30
Roy Dyckhoff, Mehrnoosh Sadrzadeh and Julien Truffaut
Algebra, Proof Theory and Applications for a Logic
of Propositions, Actions and Adjoint Modal Operators
11:30-12:00
Wolfgang Jeltsch
Towards a Common Categorical Semantics for Linear-Time
Temporal Logic and Functional Reactive Programming
12:00-13:30 Lunch
13:30-14:30 Plenary Address
Dexter Kozen
New
14:30-14:50 Break
14:50-15:20
Robin Cockett, Ximo Diaz-Boils, Jonathan Gallagher and Pavel Hrubes
Timed Sets, Functional Complexity, and Computability
15:20-15:50
Ulrich Berger and Tie Hou
Typed vs Untyped Realizability
End of conference