=Paper=
{{Paper
|id=None
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-1010/plmmspreface.pdf
|volume=Vol-1010
}}
==None==
<pdf width="1500px">https://ceur-ws.org/Vol-1010/plmmspreface.pdf</pdf>
<pre>
PLMMS Preface

This volume contains the papers presented at PLMMS-2013: 5th International
Workshop on Programming Languages for Mechanised Mathematical Systems
2013 held on July 9, 2013 in Bath.
    There were 3 submissions. Each submission was reviewed by at 2 program
committee members. The committee decided to accept 2 papers. The program
also includes 4 invited speakers:

 – Edwin Brady – Dependently Typed Functional Programming in Idris
   Idris is a general purpose pure functional programming language with depen-
   dent types. Its syntax is influenced by Haskell and its features include full
   dependent types and records, type classes, tactic based theorem proving, to-
   tality checking and an optimising compiler with a foreign function interface.
   One of the goals of the Idris project is to bring type-based program verifi-
   cation techniques to functional programmers while still supporting efficient
   systems programming via an optimising compiler and interaction with ex-
   ternal libraries. In this talk I will introduce dependently typed programming
   using Idris, and demonstrate its features using several examples including an
   interpreter for the simply typed lambda calculus, and a verified binary adder.
 – Gilles Dowek – Checking classical proofs in an constructive proof-checker
   The Dedukti project aims at using a single proof-checker to check proofs de-
   veloped in many other provers. As some of these provers are classical and
   other constructive, we need a way to express proofs of one logic into the
   other. In this talk I will sketch various ways to express classical proofs in a
   constructive setting, focussing on the possibility to design a single logic mix-
   ing classical and constructive connectors and on the possibility to recognize
   classical proofs that are constructive by chance. This talk will be based on
   joint work with Olivier Hermant and Frédéric Gilbert.
 – Conor McBride – Problems as types
   James McKinna coined the phrase “Problems as types” to characterise the
   presentation of programming and proof (combined) as a problem-solving di-
   alogue, mediating the underlying task of constructing a well typed term. The
   resulting documents should record both sides of the story—the problems posed,
   corresponding to the type to be inhabited, and the solution strategy by which
   those problems are refined to zero or more subproblems, which are elaborated
   to terms. Our language, Epigram, took a problems-as-types approach to pro-
   gramming, based on the key realisation that the type for a “programming
   problem” can be more than just the type of a program, also giving the tem-
   plate for its invocation. Whilst dependent types are beginning to catch on,
   language designers have been at pains to make programming look as much
   like ordinary functional programming as possible. The problems-as-types ap-
   proach remains underexplored. In this talk, I shall resume that exploration,
   looking at problems-as-types approaches to type, program, and proof construc-
   tion, given recent developments in relevant underlying theories.


                                        v
 – Sergei Meshveliani – Dependent Types for an Adequate Programming of
   Algebra
   This research compares the author’s experience in programming algebra in
   Haskell and in Agda (currently the former experience is large, and the lat-
   ter is small). There are discussed certain hopes and doubts related to the
   dependently typed and verified programming of symbolic computation. This
   concerns the 1) author’s experience history, 2) algebraic class hierarchy de-
   sign, 3) proof cost overhead in evaluation and in coding, 4) other subjects.
   Various examples are considered, some questions are put.

    The first paper in this volume is an invited paper by Sergei Meshveliani, also
titled Dependent Types for an Adequate Programming of Algebra.
    We would like to thank our peer reviewers for carefully reviewing the submis-
sions and giving constructive feedback. We would also like to thank Christoph
Lange for his help in efforts in putting together this volume.


June 24, 2013                                                       Florian Rabe
Newcastle                                                         Iain Whiteside

Program Committee

David Aspinall               University of Edinburgh
Serge Autexier               DFKI
Jacques Carette              McMaster University, Computing and Software
Gabriel Dos Reis             Texas A&M University
Gudmund Grov                 Heriot-Watt University
Cezar Ionescu                Potsdam Institute for Climate Impact Research
Ewen Maclean
Florian Rabe                 Jacobs University Bremen
Claudio Sacerdoti Coen       University of Bologna
Tim Sheard                   Portland State University
Sergei Soloviev
Stephen Watt                 University of Western Ontario
Makarius Wenzel              Université Paris-Sud 11
Iain Whiteside               University of Edinburgh
Freek Wiedijk                Radboud University Nijmegen
Wolfgang Windsteiger         RISC Institute, JKU Linz, Austria




                                        vi

</pre>