|Assia Mahboubi is a permanent researcher at Inria and an endowed Professor at the Department of Mathematics of the VU Amsterdam. Her research interests are the foundations and formalization of mathematics in type theory and the automated verification of mathematical proofs. She was previously a member of the Mathematical Components team at the Inria Microsoft Research joint centre, known for a machine-checked proof of the Odd Order theorem in finite group theory. She has been one of the main contributors to this collaborative effort. Her current projects are related to the formal verification of mathematical software.|
|Annabelle McIver is a Professor of Computer Science at Macquarie University in Sydney. Annabelle trained as a mathematician at Cambridge and Oxford Universities. Her research uses mathematics to prove quantitative properties of programs, and more recently to provide foundations for quantitative information flow for analysing security properties. She is co-author of the book Abstraction, Refinement and Proof for Probabilistic Systems, and of the forthcoming title The Science of Quantitative Information Flow.|
|Tony Hoare's highest official academic qualification is an MA in Classical Greats at Oxford (1952-1956). He earned professional qualifications as an Interpreter of Russian (1956-8) and as a Statistician (1958-9). He exercised his Russian as an intern at Moscow State University (1959-60), and on many subsequent visits to the Soviet Union (or Russia) and to Armenia. His first job was in the UK Computer Industry at a small computer manufacturer, where he held posts as Programmer, Chief Engineer, and Researcher (1960-68). He then applied for the Chair of Computing Science at the Queen’s University, Belfast, and to his surprise he was appointed (1968-77). He left Belfast with regret, to return to Oxford University as Professor of Computation back at Oxford (1977-99). His first retirement job was in Cambridge with Microsoft Research (1999-2017) where he stimulated an international Grand Challenge Initiative in Verified Software. Since his second retirement, he has been an unpaid Visitor at Microsoft Research and an Honorary Member of the Cambridge University Computing Laboratory. (UTP keynote open to MPC particpants.)|
|Shriram Krishnamurthi is a Professor of Computer Science and an Associate Director of the Executive Master in Cybersecurity at Brown University. With collaborators and students, he has created several influential systems and written multiple widely-used books. He also co-directs the Bootstrap math-and-computing outreach program. For his work he has received SIGPLAN’s Robin Milner Young Researcher Award, SIGSOFT’s Influential Educator Award, SIGPLAN’s Software Award, and Brown’s Henry Merritt Wriston Fellowship for distinguished contribution to undergraduate education. He has authored over a dozen papers recognized for honors by program committees. He has an honorary doctorate from the Università della Svizzera Italiana. (FM keynote open to MPC participants.)|
The Mean-Tempered Keyboard: Coding with Asymmetric Numeral Systems
An Analysis of Repeated Graph Search
Verified Self-Explaining Computation
Jan Stolarek and James Cheney
A Hierarchy of Monadic Effects for Program Verification using Equational Reasoning
Reynald Affeldt, David Nowak and Takafumi Saikawa
Setoid Type Theory --- A Syntactic Translation
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi and Nicolas Tabareau
En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad
Niccolò Veltri and Robin Kaarsgaard
Certification of Breadth-First Algorithms by Extraction
Dominique Larchey-Wendling and Ralph Matthes
Completeness and Incompleteness of Synchronous Kleene Algebra
Jana Wagemaker, Tobias Kappé, Jurriaan Rot, Marcello Bonsangue and Alexandra Silva
Handling Local State with Global State
Koen Pauwels, Tom Schrijvers and Shin-Cheng Mu
Cylindric Kleene Lattices for Program Construction
Brijesh Dongol, Ian J. Hayes, Larissa Meinicke and Georg Struth
Shallow Embedding of Type Theory is Morally Correct
Ambrus Kaposi, András Kovács and Nicolai Kraus
Experiments in Information Flow Analysis (invited paper)
How to Calculate with Nondeterministic Functions
Richard Bird and Florian Rabe
System F in Agda, for Fun and Profit
James Chapman, Roman Kireev, Chad Nester and Philip Wadler
Unraveling Recursion: Compiling an IR with Recursion to System F
Roman Kireev, Chad Nester, Michael Peyton Jones, Philip Wadler, Vasilis Gkoumas and Kenneth MacKenzie
Self-Certifying Railroad Diagrams, Or: How to Teach Nondeterministic Finite Automata
The conference program is available here.
The International Conference on Mathematics of Program Construction (MPC) aims to promote the development of mathematical principles and techniques that are demonstrably practical and effective in the process of constructing computer programs.
MPC 2019 will be held in Porto, Portugal from 7-9 October 2019, and is co-located with the International Symposium on Formal Methods, FM 2019.
Previous conferences were held in
Königswinter, Germany (2015);
Madrid, Spain (2012);
Québec City, Canada (2010);
Marseille, France (2008);
Kuressaare, Estonia (2006);
Stirling, UK (2004);
Dagstuhl, Germany (2002);
Ponte de Lima, Portugal (2000);
Marstrand, Sweden (1998);
Kloster Irsee, Germany (1995);
Oxford, UK (1992);
Twente, The Netherlands (1989).
MPC seeks original papers on mathematical methods and tools put to use in program construction. Topics of interest range from algorithmics to support for program construction in programming languages and systems. Typical areas include type systems, program analysis and transformation, programming language semantics, security, and program logics. The notion of a 'program' is interpreted broadly, ranging from algorithms to hardware.
Theoretical contributions are welcome, provided that their relevance
to program construction is clear. Reports on applications are welcome,
provided that their mathematical basis is evident. We also encourage
the submission of 'programming pearls' that present elegant and
instructive examples of the mathematics of program construction.
Submission is in two stages. Abstracts (plain text, maximum 250 words) must be submitted by 7th May 2019. Full papers (pdf, formatted using the llncs.sty style file for LaTex) must be submitted by 10th May 2019. There is no prescribed page limit, but authors should strive for brevity. Both abstracts and papers will be submitted using EasyChair.
Papers must present previously unpublished work, and not be submitted concurrently to any other publication venue. Submissions will be evaluated by the program committee according to their relevance, correctness, significance, originality, and clarity. Each submission should explain its contributions in both general and technical terms, clearly identifying what has been accomplished, explaining why it is significant, and comparing it with previous work. Accepted papers must be presented in person at the conference by one of the authors.
The proceedings of MPC 2019 will be published in the Lecture Notes in Computer Science (LNCS) series, as with all previous instances of the conference. Authors of accepted papers will be expected to transfer copyright to Springer for this purpose.
After the conference, authors of the best papers from MPC 2019 and MPC 2015 will be invited to submit revised versions to a special issue of Science of Computer Programming (SCP).
For any queries about submission please contact the program chair,
|Patrick Bahr||IT University of Copenhagen, Denmark|
|Richard Bird||University of Oxford, UK|
|Corina Cîrstea||University of Southampton, UK|
|Brijesh Dongol||University of Surrey, UK|
|João F. Ferreira||University of Lisbon, Portugal|
|Jennifer Hackett||University of Nottingham, UK|
|William Harrison||University of Missouri, USA|
|Ralf Hinze||University of Kaiserslautern, Germany|
|Zhenjiang Hu||Peking University, China|
|Graham Hutton (chair)||University of Nottingham, UK|
|Cezar Ionescu||University of Oxford, UK|
|Mauro Jaskelioff||National University of Rosario, Argentina|
|Ranjit Jhala||University of California, USA|
|Gabriele Keller||Utrecht University, The Netherlands|
|Ekaterina Komendantskaya||Heriot-Watt University, UK|
|Chris Martens||North Carolina State University, USA|
|Bernhard Möller||University of Augsburg, Germany|
|Shin-Cheng Mu||Academia Sinica, Taiwan|
|Mary Sheeran||Chalmers University of Technology, Sweden|
|Alexandra Silva||University College London, UK|
|Georg Struth||University of Sheffield, UK|
The conference will be held at the Alfândega Porto Congress Centre, a 150 year old former custom's house located in the historic centre of Porto on the bank of the river Douro. The venue was renovated by a Pritzer prize winning architect and has received many awards.
Registration and travel information is available here.
|José Nuno Oliveira||University of Minho, Portugal|
For any queries about local issues please contact the local organiser,
José Nuno Oliveira.