Sergei Meshveliani | 29 Oct 16:25 2014

`with' -> `case' example

Please, how to rewrite the below `with' in  keys-commute-delByKey
to `case' ?
The `with' variant is type-checked (in Agda-2.4.2), the `case' one does



open import Function using (_∘_; case_of_)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Unary   using (Decidable)
open import Relation.Binary  using (module Setoid; module DecSetoid; 
                             renaming (Decidable to Decidable₂)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≗_)
open import Data.Product using (_×_; proj₁; _,_)
open import Data.List    using (List; []; _∷_; map)

delBy : ∀ {α p} {A : Set α} {P : A → Set p} →
                            (P? : Decidable P) → List A → List A
delBy _  []       = []
delBy P? (x ∷ xs) = case P? x of \ { (yes _) → xs
                                   ; (no _)  → x ∷ (delBy P? xs) }

module AssocList-pack {α α= β} (Key : DecSetoid α α=) (Val : Set β)
(Continue reading)

Jesper Cockx | 29 Oct 10:44 2014

Puzzled about how instance arguments work in the presence of metas

Can someone tell me if the code fragment below is supposed to work? It gives me yellow, but it works fine when I replace `it` by the (unique) solution `is-zero`.

it : {A : Set} {{_ : A}} → A
it {{x}} = x

data IsZero : Nat → Set where
    is-zero : IsZero 0

test : IsZero _
test = it

Agda mailing list
Sergei Meshveliani | 25 Oct 17:18 2014

ℕ ⊆ P U Q -> ¬ isFinite P or ...


I have been asked about a constructive proof of this theorem:

  ℕ ⊆ P U Q -> (¬ isFinite P) ⊎ (¬ isFinite Q).

A subset in ℕ is defined as an algorithmic predicate  P : ℕ -> Set.

setℕ (total set),  _⊆_,  P,  _U_ (union)  
are defined in a natural way, via predicates.

Finiteness is defined as 

  _Enumerates_ : List ℕ → NSet → Set _
  xs Enumerates P =
                    {x : ℕ} → P x → x ∈ xs

  isFinite : NSet → Set _
  isFinite P =  ∃ \xs → xs Enumerates P

I have proved this in Agda:

 ⋃isFiniteIfBoth : {P Q : NSet} → isFinite P → isFinite Q → 
                                               isFinite (P ⋃ Q),

 theorem1 : {P Q : NSet} → setℕ ⊆ (P ⋃ Q) → ¬ (isFinite P × isFinite Q).

And I have an impression that the statement 

 question : {P Q : NSet} → setℕ ⊆ (P ⋃ Q) → 
                                       (¬ isFinite P) ⊎ (¬ isFinite Q)

has not a constructive proof.

Has it?


Andreas Abel | 24 Oct 18:37 2014

ICALP 2015 first call for papers

Please consider submitting a paper to ICALP 2015 in the beautiful Kyoto. 
  Submissions accepted until 17 Feb 2015.

			      ICALP 2015


			First Call for Papers

The 42nd International Colloquium on Automata, Languages, and
Programming (ICALP) will take place in the period 6-10 July 2015 in
Kyoto, Japan. The conference will co-locate with LICS 2015, the 30th
ACM/IEEE Symposium on Logic in Computer Science. The ICALP 2015
conference chair is Kazuo Iwama (Kyoto University).

ICALP is the main conference and annual meeting of the European
Association for Theoretical Computer Science (EATCS). As usual, the
main conference will be preceded and/or followed by a series of

Important dates

Submission deadline: Tuesday, 17 February 2015, 23:59 PST (Pacific 
Standard Time, UTC-8)
Author notification: 15 April 2015
Final manuscript due: 30 April 2015

Deadlines are firm; late submissions will not be considered.


ICALP proceedings are published in the Springer-Verlag ARCoSS
(Advanced Research in Computing and Software Science) subseries of
LNCS (Lecture Notes in Computer Science).

Invited Speakers

Ken Kawarabayashi, NII, Japan
Valerie King, University of Victoria, Canada
Thomas Moscibroda, MSR Asia, China
Anca Muscholl, Universitè Bordeaux, France (Joint with LICS)
Peter O'Hearn, Facebook, UK (Joint with LICS)

Invited Tutorial Speakers (Joint with LICS)
Piotr Indyk, MIT, USA
Andrew Pitts, University of Cambridge, UK
Geoffrey Smith, Florida International University, USA

Masterclass speaker
Ryuhei Uehara, JAIST, Japan


Papers presenting original research on all aspects of theoretical
computer science are sought. Typical but not exclusive topics of
interest are:

Track A: Algorithms, Complexity and Games

* Algorithmic Game Theory
* Approximation Algorithms
* Combinatorial Optimization
* Combinatorics in Computer Science
* Computational Biology
* Computational Complexity
* Computational Geometry
* Cryptography
* Data Structures
* Design and Analysis of Algorithms
* Machine Learning
* Parallel, Distributed and External Memory Computing
* Randomness in Computation
* Quantum Computing

Track B: Logic, Semantics, Automata and Theory of Programming

* Algebraic and Categorical Models
* Automata, Games, and Formal Languages
* Emerging and Non-standard Models of Computation
* Databases, Semi-Structured Data and Finite Model Theory
* Principles and Semantics of Programming Languages
* Logic in Computer Science, Theorem Proving and Model Checking
* Models of Concurrent, Distributed, and Mobile Systems
* Models of Reactive, Hybrid and Stochastic Systems
* Program Analysis and Transformation
* Specification, Refinement, Verification and Synthesis
* Type Systems and Theory, Typed Calculi

Track C: Foundations of Networked Computation:
          Models, Algorithms and Information Management

* Algorithmic Aspects of Networks and Networking
* Formal Methods for Network Information Management
* Foundations of Privacy, Trust and Reputation in Networks
* Mobile and Wireless Networks and Communication
* Network Economics and Incentive-Based Computing Related to Networks
* Networks of Low Capability Devices
* Network Mining and Analysis
* Overlay Networks and P2P Systems
* Specification, Semantics, Synchronization of Networked Systems
* Theory of Security in Networks

Submission Guidelines

Authors are invited to submit an extended abstract of no more than 12
pages, including references, in LNCS style presenting original
research on the theory of Computer Science.  All submissions will be
electronic via the EasyChair page for the conference, with three
tracks (A, B and C):

Submissions should be made to the appropriate track of the conference.
No prior publication or simultaneous submission to other publication
outlets (either a conference or a journal) is allowed.

Submissions must adhere to the specified format and
length. Submissions that are too long or formatted incorrectly may be
rejected immediately.  All the technical details that are necessary
for a proper scientific evaluation of a submission must be included in
a clearly-labelled appendix, to be consulted at the discretion of
program committee members. This includes, in particular, the proofs of
all the key theorems in a paper.

Should I submit my paper to Track A or Track C?

While the scope of Tracks A and B are generally well understood given
their long history, the situation for Track C may be less obvious. In
particular, some clarifications may be helpful regarding areas of
potential overlap, especially between Tracks A and C.

The aim for Track C is to be the leading venue for theory papers truly
motivated by networking applications, and/or proposing theoretical
results relevant to real networking, certified analytically, but not
necessarily tested practically. The motivation for the track was the
lack of good venues for theory papers motivated by applications in
networking. On the one hand, the good networking conferences typically
ask for extended experiments and/or simulations, while the TCS
community is hardly able to do such experiments or simulations. On the
other hand, the good conferences on algorithms tend to judge a paper
based only on its technical difficulty and on its significance from an
algorithmic perspective, which may not be the same as when judging the
paper from the perspective of impact on networks.

Several areas of algorithmic study of interest to track C have a broad
overlap with track A. Graph algorithmics can belong in either, though
if the work is not linked to networking, it is more appropriate in
track A. Algorithmic game theory is another area of major
overlap. Aspects involving complexity, the computation of equilibria
and approximations, belong more in Track A, while results with
applications in auctions, networks and some aspects of mechanism
design belong in Track C.

Finally, it should be noted that algorithms and complexity of
message-passing based distributed computing belong squarely in track
C, while certain other aspects of distributed computing do not fall
under its scope.

Best Paper Awards

As in previous editions of ICALP, there will be best paper and best
student paper awards for each track of the conference. In order to be
eligible for a best student paper award, a paper should be authored
only by students and should be marked as such upon submission.


Track A: Algorithms, complexity, and games

Peyman Afshani, Aarhus University, Denmark
Hee-Kap Ahn, POSTECH, South Korea
Hans Bodlaender Utrecht University, The Netherlands
Karl Bringmann, Max-Planck Institut für Informatik, Germany
Sergio Cabello, University of Ljubljana, Slovenia
Ken Clarkson, IBM Almaden Research Center, USA
Éric Colin de Verdière, École Normale Supérieure Paris, France
Stefan Dziembowski, University of Warsaw, Poland
David Eppstein, University of California at Irvine, USA
Dimitris Fotakis, National Technical University of Athens, Greece
Paul Goldberg, University of Oxford, UK
MohammadTaghi Hajiaghayi, University of Maryland at College Park, USA
Jesper Jansson, Kyoto University, Japan
Andrei Krokhin, Durham University, UK
Asaf Levin, Technion, Israel
Inge Li Gørtz, Technical University of Denmark, Denmark
Pinyan  Lu, Microsoft Research Asia, China
Frédéric Magniez, Université Paris Diderot, France
Kazuhisa Makino, Kyoto University, Japan
Elvira	Mayordomo, Universidad de Zaragoza, Spain
Ulrich Meyer, Goethe University Frankfurt am Main, Germany
Wolfgang Mulzer, Free University Berlin, Germany
Viswanath Nagarajan, University of Michigan, USA
Vicky Papadopoulou, European University Cyprus, Cyprus
Michał 	Pilipczuk, University of Bergen, Norway
Liam Roditty, Bar-Ilan University, Israel
Ignaz Rutter, Karlsruhe Institute of Technology, Germany
Rocco Servedio, Columbia University, USA
Jens Schmidt, TU Ilmenau, Germany
Bettina Speckmann (chair), TU Eindhoven, The Netherlands
Csaba D. Tóth, California State University Northridge, USA
Takeaki Uno, National Institute of Informatics, Japan
Erik Jan van Leeuwen, Max-Planck Institut für Informatik, Germany
Rob van Stee, University of Leicester, UK
Ivan Visconti, University of Salerno, Italy

Track B: Logic, semantics, automata and theory of Programming

Andreas Abel, Chalmers and Gothenburg University, Sweden
Albert Atserias, Universitat Politècnica de Catalunya, Spain
Christel Baier, TU Dresden, Germany
Lars Birkedal, Aarhus University, Denmark,
Luís Caires, Universidade Nova de Lisboa, Portugal
James Cheney, University of Edinburgh, UK
Wei Ngan Chin, National University of Singapore, Singapore
Ugo Dal Lago, University of Bologna, Italy
Thomas Ehrhard, CNRS, Université Paris Diderot, France
Zoltán Ésik, University of Szeged, Hungary
Xinyu Feng, University of Science and Technology of China, China
Wan Fokkink, VU University Amsterdam, The Netherlands
Shin-ya Katsumata, Kyoto University, Japan
Naoki Kobayashi (chair), The University of Tokyo, Japan
Eric Koskinen, New York University, USA
Antonín Kučera, Masaryk University, Czech Republic
Orna Kupferman, Hebrew University, Israel
Annabelle Mclver, Macquarie University, Australia
Dale Miller, INRIA Saclay, France
Markus Müller-Olm, University of Münster, Germany
Andrzej Murawski, Univeristy of Warwick, UK
Joel Ouaknine, Univeristy of Oxford, UK
Prakash Panangaden, McGill University, Canada
Pawel Parys, University. of Warsaw, Poland
Reinhard Pichler, TU Vienna, Austria
Simona Ronchi Della Rocca, University of Torino, Italy
Jeremy Siek, Indiana University, USA

Track C: Foundations of networked computation:
          Models, algorithms and information management

Ioannis Caragiannis, Univ. Patras, Greece
Katarina Cechlarova, Pavol Jozef Safarik Univ., Slovakia
Shiri Chechik, Tel Aviv Univ., Israel
Yuval Emek, Technion, Israel
Sándor Fekete, TU Braunschweig, Germany
Pierre Fraigniaud, CNRS and Paris Diderot, France
Leszek Gąsieniec, Univ. Liverpool, UK
Aristides Gionis, Aalto Univ., Finland
Magnús M. Halldórsson (chair), Reykjavik Univ, Iceland
Monika Henzinger, Univ. Wien, Austria
Bhaskar Krishnamachari, USC, USAL
Fabian Kuhn, Freiburg, Germany
Michael Mitzenmacher, Harvard Univ, USA
Massimo Merro, Univ. Verona, Italy
Gopal Pandurangan, Univ. Houston, USA
Pino Persiano, Salerno, Italy
R. Ravi, CMU, USA
Ymir Vigfusson, Emory Univ., USA
Roger Wattenhofer, ETH Zurich, Switzerland
Masafumi Yamashita, Kyushu Univ., Japan


Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

Mateusz Kowalczyk | 23 Oct 02:02 2014

Info on interacting with the Agda process


Say I wanted to talk to Agda like emacs does: get all the type info,
highlighting &c &c. Is there a place where this process is documented,
notably the format that's expected both ways or is looking at the ELisp
and Haskell source the only way?

I would also ask whether we could just talk to Agda directly, cutting
out the process and parsing of the information: say we can talk to
Haskell natively, would it be viable to just talk straight to the Agda
library or would it be awkward to do so? I can imagine a much better
degree of freedom with this approach but I don't know whether it was
ever intended to be used this way. Notably, the package on Hackage says
“Note that the Agda library does not follow the package versioning
policy, because it is not intended to be used by third-party packages.”.



Mateusz K.
Michael Winter | 20 Oct 21:19 2014

CFP: Relational and Algebraic Methods in Computer Science (RAMiCS 2015)

                           CALL FOR PAPERS

                  15th International Conference on
    Relational and Algebraic Methods in Computer Science (RAMiCS 2015)

            28 September to 1 October 2015, Braga, Portugal


 We invite submissions in the general area of Relational and Algebraic 
 Methods  in Computer Science. Special focus will lie on formal methods 
 for software engineering, logics of programs and links with neighbouring 

 Particular topics of interest for the conference cover,
 but are not limited to:

 * Algebraic approaches to
   - specification, development, verification, and analysis of programs
     and algorithms
   - computational logic, in particular logics of programs, modal and
     dynamic logics, interval and temporal logics
   - semantics of programming languages

 * Applications in fields such as
   - relational formal methods such as B or Z, tabular methods
   - information systems
   - graph theory and combinatorial optimisation
   - games, automata and language theory
   - spatio-temporal reasoning, knowledge acquisition
   - preference and scaling methods, computational social choice,
     social software

 * Theoretical foundations and supporting tools, including
   - mechanised and automated reasoning, decision procedures
   - process algebras, fixed point calculi, idempotent semirings,
     quantales, allegories
   - dynamic algebras, cylindric algebras and their applications in 


 Since 1994, the RelMiCS meetings on Relational Methods in Computer 
 Science have been a main forum for researchers who use the calculus of 
 relations and similar algebraic formalisms as methodological and 
 conceptual tools. The AKA workshop series on Applications of Kleene 
 algebra started with a Dagstuhl seminar in 2001 and was co-organised 
 with the RelMiCS conference until 2009. Since 2011, joint RAMiCS 
 conferences continue to encompass the scope of both RelMiCS and AKA.

 The predecessors of this conference were held in Dagstuhl (January 
 1994), Parati (September 1995), Hammamet (January 1997), Warsaw 
 (September 1998), Quebec (January 2000), Dagstuhl (February 2001), 
 Oisterwijk (October 2001), Malente (April 2003), St. Catharines 
 (January 2005), Manchester (September 2006), Frauenwoerth (April 2008), 
 Doha (November 2009), Rotterdam (June 2011), Cambridge UK (September 
 2012) and Marienstatt im Westerwald (April 2014).

 Student Program

 The conference will be accompanied by a PhD training program. Details 
 will be published in due time in a special call and on the conference 

 Proceedings and Submission

 All papers will be formally reviewed. We plan to publish the
 proceedings in the series Lecture Notes in Computer Science ready at
 the conference. Submissions must be in English, in Postscript or PDF
 format, and provide sufficient information to judge their merits.
 They must be unpublished and not submitted for publication elsewhere. 
 They should not exceed 16 pages in Springer LNCS style (accepted
 papers must be produced with LaTeX). Additional material may be
 provided by a clearly marked appendix or a reference to a manuscript
 on a website. This may be considered at the discretion of the PC.
 Deviation from these requirements may cause immediate rejection.
 One author of each accepted paper is expected to present the paper
 at the conference.

 Submission is via EasyChair at the following address:
 Formatting instructions and the LNCS styled files can be obtained via:

 As for the earlier conferences of this series, it is also intended to
 publish a selection of the best papers in revised and extended form in
 a special issue of the Journal of Logic and Algebraic Methods in
 Programming (JLAMP).

 Important Dates

     Title and abstract submission:                 March 18 2015
     Submission of full papers:                     March 26 2015
     Notification:                                  June  05 2015
     Final versions due (firm deadline):            July  10 2015

     Conference:                   September 28 - October 01 2015

 Programme Committee

     Rudolf Berghammer     (Kiel, Germany)
     Jules Desharnais      (Laval U., Canada)
     Marcelo Frias         (Buenos Aires, Argentina)
     Stephen Givant        (Mills College, USA)
     Hitoshi Furusawa      (Kagoshima, Japan)
     Timothy G. Griffin    (Cambridge, UK)
     Walter Guttmann       (Canterbury, New Zealand)
     Robin Hirsch          (London, UK)
     Peter Hoefner         (NICTA, Australia; Publicity chair)
     Ali Jaoua             (Doha, Qatar)
     Peter Jipsen          (Chapman U., USA)
     Wolfram Kahl          (McMaster U., Canada)
     Rodger Maddux         (Iowa State U., USA)
     Ali Mili              (NJIT, U. Heights, USA)
     Bernhard Moeller      (U. Augsburg, Germany)
     Martin E. Mueller     (U. Augsburg, Germany)
     Jose N. Oliveira      (U. Minho, Portugal; General chair)
     Ewa Orlowska          (Warsaw, Poland)
     Agnieszka Rusinowska  (Univ. Paris 1, France)
     Gunther Schmidt       (Munich, Germany)
     Renate Schmidt        (Manchester, UK)
     Isar Stubbe           (U. Littoral-Cote-d'Opale, France)
     Michael Winter        (Brock U., Canada; PC chair)


 Steering Committee

     Rudolf Berghammer  (Kiel, Germany)
     Jules Desharnais   (Laval U., Canada)
     Ali Jaoua          (Doha, Qatar)
     Peter Jipsen       (Chapman U., USA)
     Bernhard Moeller   (U. Augsburg, Germany)
     Jose N. Oliveira   (U. Minho, Portugal)
     Ewa Orlowska       (Warsaw, Poland)
     Gunther Schmidt    (Munich, Germany)
     Michael Winter     (Brock U., Canada)


 Organising Committee

     Jose N. Oliveira    (U. Minho, Portugal; General chair)
     Michael Winter      (Brock U., Canada; PC chair)
     Luis S. Barbosa     (U. Minho, Portugal)
     Manuel A. Cunha     (U. Minho, Portugal)
     Antonio N. Ribeiro  (U. Minho, Portugal)
Sergei Meshveliani | 19 Oct 18:06 2014

explicit irrelevance question

Dear Agda developers,

can you, please tell whether the below statement  g=f-if
must have a proof in Agda ?
If yes, then what can be a proof ?

(I am stuck with both explicit irrelevance and a dot-annotated



open import Level            using (_⊔_)
open import Function         using (case_of_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary  using (module IsEquivalence;
                                    module DecSetoid; DecSetoid)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Empty using (⊥-elim)

module _ {α α=} (A : DecSetoid α α=) (0# : DecSetoid.Carrier A)
  open DecSetoid A using (_≈_; _≟_; isEquivalence)
                                    renaming (Carrier to C)
  open IsEquivalence isEquivalence renaming (refl to ≈refl)

  record Foo : Set (α ⊔ α=)
    field f       : (x : C) → ¬ x ≈ 0# → C
          irrel-f : (x : C) → (nz nz' : ¬ x ≈ 0#) → f x nz ≈ f x nz'

    g : C → C
    g x  with x ≟ 0#
    ...             | yes _  = x
    ...             | no x≉0 = f x x≉0

    g=f-if : ∀ x → (x≉0 : ¬ x ≈ 0#) → g x ≈ f x x≉0
    g=f-if x x≉0  with x ≟ 0#
    ...                      | yes x=0 = ⊥-elim (x≉0 x=0)
    ...                      | no x/=0 = ≈refl
                                         -- ?
Helmut Grohne | 15 Oct 13:15 2014

Internal error at src/full/Agda/TypeChecking/Substitute.hs:144

Dear Agda developers,

While refactoring some Agda code I ran into the following error message:

| Checking Error (../full/path/to/Error.agda).
| An internal error has occurred. Please report this as a bug.
| Location of the error: src/full/Agda/TypeChecking/Substitute.hs:144

This is produced using Agda 2.4.2 as obtained using cabal on a Linux
amd64 system with GHC 7.6.3.

I went ahead and tried to find a reproducer with less than 1000 lines.
After feeding Agda 30000 samples, I came up with the following 7 lines:

data A (B : Set) : Set where
module C where
  record D : Set where
module E (F : Set) (G : A F) where
  open C public using (module D)
module H (I : Set) (J : A I) where
  open E I J using ()

Is this also reproducible on the development version of Agda?

Andrew Harris | 14 Oct 04:13 2014

simple question


   I'm trying to follow along in the very good paper "Dependent Types At Work" written by Ana Bove and Peter Dybjer.  I'm stuck at trying to prove "eq-succ", which is one of the exercises in Section 4.4.  The closest I can make it is the following:

{- proof of eq-succ -}
eq-succ : {n m : Nat} → n == m → succ n == succ m
eq-succ (refl m) = natrec {(\k → (k + m) == (plus k m))} (refl m) (\i h → ((succ i) + m) == (plus (succ i) m)) m

But this does not typecheck, I get the error:

Set !=< (succ i + m) == plus (succ i) m of type Set₁
when checking that the expression (succ i + m) == plus (succ i) m
has type (succ i + m) == plus (succ i) m

I'm stuck -- I don't quite understand what I'm supposed to create an element of Set_1 that has a signature of (succ i + m) == plus (succ i) m, (if that's what I'm supposed to do).  Any hints would be appreciated!

Agda mailing list
Pepijn Kokke | 12 Oct 13:28 2014

Expanding literate Agda

Dear all,

I've implemented a pre-processor to "unlit" various styles of literate code, i.e. LaTeX-style, bird tags, Markdown-style code blocks, etcetera. I'm currently trying to integrate it into Agda. There are currently two proposals for how to do this.

The first is the following:

Try to infer the literate format from the file, making it explicit with Agda command-line arguments if necessary. 
This would mean that, for instance, if the "unlit" program would encounter a "\begin{code}" tag, it would assume the literate Agda file was was written in LaTeX style, if it encountered a "```" fence it would assume Markdown, etcetera... 
(I would personally prefer that a bird tag would also indicate Markdown, because the two formats integrate so well and are already used in this manner in the Haskell community.)
The advantages of this approach is that it can easily be integrated into the current Agda, and all literate files would have the .lagda extension.
In the case where it is desirable to mix formats in a strange way (i.e. mix bird tags and LaTeX or even LaTeX blocks and Markdown blocks) command-line arguments could be passed to Agda explicitly stating the literate style---though I'm guessing this would never be necessary.

The second proposal is the following:

Each style of literate Agda would have its own extension. For instance: LaTeX-style would ".agda.tex", Markdown would use "" and Bird-style would use ".agda.txt". 
The advantages of this approach is that there is no inference needed, as the format will be unambiguously specified in the extension. 
The problem with this approach is that it will require modifications to many parts of the Agda ecosystem. For instance, the code that resolves module names to files would have to change to also take ".agda.tex" and such into consideration. The same modifications would probably have to be made for the Emacs (and other) editing mode. This would constitute many (trivial) changes across the Agda codebase. 

I'd like to hear your thoughts on these different approaches, or---if you have proposals of dealing with this in a different manner---how you would solve this problem.

Agda mailing list
José Pedro Magalhães | 10 Oct 14:58 2014

Mathematics of Program Construction (MPC 2015): first call for papers

Apologies for multiple copies.


12th International Conference on Mathematics of Program Construction (MPC 2015)
Königswinter, Germany, 29 June - 1 July 2015


The MPC conferences aim to promote the development of mathematical principles
and techniques that are demonstrably practical and effective in the process of
constructing computer programs, broadly interpreted.

The 2015 MPC conference will be held in Königswinter, Germany, from 29th June to
1st July 2015. The previous conferences were held in Twente, The Netherlands
(1989), Oxford, UK (1992), Kloster Irsee, Germany (1995), Marstrand, Sweden
(1998), Ponte de Lima, Portugal (2000), Dagstuhl, Germany (2002), Stirling, UK
(2004, colocated with AMAST), Kuressaare, Estonia (2006, colocated with AMAST),
Marseille, France (2008), Québec City, Canada (2010, colocated with AMAST), and
Madrid, Spain (2012).


Papers are solicited 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. The notion of "program" is
broad, from algorithms to hardware. Some typical areas are type systems, program
analysis and transformation, programming-language semantics, security, and
program logics. 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 "pearls": elegant, instructive, and fun
essays on the mathematics of program construction.


   * Submission of abstracts:      26 January 2015
   * Submission of full papers:     2 February 2015
   * Notification to authors:      16 March 2015
   * Final version:                13 April 2015


Submission is in two stages. Abstracts (plain text, 10 to 20 lines) must be
submitted by 26 January 2015. Full papers (pdf) adhering to the LaTeX llncs
style must be submitted by 2 February 2015. There is no official page limit, but
authors should strive for brevity. The web-based system EasyChair will be used

Papers must report previously unpublished work, and must not be submitted
concurrently to a journal or to another conference with refereed proceedings.
Accepted papers must be presented at the conference by one of the authors.
Please feel free to write to mpc2015-bC77Qfv0vuxrovVCs/ with any questions
about academic matters.

The proceedings of MPC 2015 will be published in Springer-Verlag's Lecture Notes
in Computer Science series, as have all the previous editions. Authors of
accepted papers will be expected to transfer copyright to Springer for this
purpose. After the conference, authors of the best papers will be invited to
submit revised versions to a special issue of the Elsevier journal Science of
Computer Programming.


Ralf Hinze                University of Oxford, UK (chair)

Eerke Boiten              University of Kent, UK
Jules Desharnais          Université Laval, Canada
Lindsay Groves            Victoria University of Wellington, New Zealand
Zhenjiang Hu              National Institute of Informatics, Japan
Graham Hutton             University of Nottingham, UK
Johan Jeuring             Utrecht University and Open University, The Netherlands
Jay McCarthy              Vassar College, US
Bernhard Möller           Universität Augsburg, Germany
Shin-Cheng Mu             Academia Sinica, Taiwan
Dave Naumann              Stevens Institute of Technology, US
Pablo Nogueira            Universidad Politécnica de Madrid, Spain
Ulf Norell                University of Gothenburg, Sweden
Bruno C. d. S. Oliveira   The University of Hong Kong, Hong Kong
José Nuno Oliveira        Universidade do Minho, Portugal
Alberto Pardo             Universidad de la República, Uruguay
Christine Paulin-Mohring  INRIA-Université Paris-Sud, France
Tom Schrijvers  KU Leuven, Belgium
Emil Sekerinski           McMaster University, Canada
Tim Sheard                Portland State University, US
Anya Tafliovich           University of Toronto Scarborough, Canada
Tarmo Uustalu             Institute of Cybernetics, Estonia
Janis Voigtländer         Universität Bonn, Germany


The conference will take place in Königswinter, Maritim Hotel, where
accommodation has been reserved. Königswinter is situated on the right bank of
the river Rhine, opposite Germany's former capital Bonn, at the foot of the


Ralf Hinze                      University of Oxford, UK (co-chair)
Janis Voigtländer               Universität Bonn, Germany (co-chair)
José Pedro Magalhães            University of Oxford, UK
Nicolas Wu                      University of Oxford, UK

For queries about local matters, please write to

Agda mailing list