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 Méllies (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 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]