Wouter Swierstra | 26 May 13:14 2016

CFP: Workshop on Type-driven Development (TyDe '16)

                             FINAL CALL FOR PAPERS

                     1st Type-Driven Development (TyDe '16)
                                 A Workshop on
                   Dependently Typed and Generic Programming

                           18 September, Nara, Japan

The deadline of the inaugural edition of TyDe is approaching rapidly.
Please submit full papers before June 10th and abstracts before
June 24th.

# Goals of the workshop

The workshop on Type-Driven Development aims to show how static type
information may be used effectively in the development of computer
programs. The workshop, co-located with ICFP, unifies two workshops: the
Workshop on Dependently Typed Programming and the Workshop on Generic

These two research areas have a rich history and bridge both theory and
practice. Novel techniques explored by both communities has gradually
spread to more mainstream languages. This workshop aims to bring
together leading researchers and practitioners in generic programming
and dependently typed programming from around the world, and features
papers capturing the state of the art in these important areas.

We welcome all contributions, both theoretical and practical, on:

-   dependently typed programming;
-   generic programming;
-   design and implementation of programming languages, exploiting types
    in novel ways;
-   exploiting typed data, data dependent data, or type providers;
-   static and dynamic analyses of typed programs;
-   tools, IDEs, or testing tools exploiting type information;
-   pearls, being elegant, instructive examples of types used in the
    derivation, calculation, or construction of programs.

# Program Committee

-   James Chapman, University of Strathclyde (co-chair)
-   Wouter Swierstra, University of Utrecht (co-chair)
-   David Christiansen, Indiana University
-   Pierre-Evariste Dagand, LIP6
-   Richard Eisenberg, University of Pennsylvania
-   Catalin Hritcu, INRIA Paris
-   James McKinna, University of Edinburgh
-   Keiko Nakata, FireEye
-   Tomas Petricek, University of Cambridge
-   Birgitte Pientka, McGill University
-   Tom Schrijvers, KU Leuven
-   Makoto Takeyama, Kanagawa University
-   Nicolas Wu, University of Bristol
-   Brent Yorgey, Hendrix College

# Proceedings and Copyright

We plan to have formal proceedings, published by the ACM. Accepted
papers will be included in the ACM Digital Library. Authors must grant
ACM publication rights upon acceptance, but may retain copyright if they
wish. Authors are encouraged to publish auxiliary material with their
paper (source code, test data, and so forth). The proceedings will be
freely available for download from the ACM Digital Library from one week
before the start of the conference until two weeks after the conference.

# Submission details

Submitted papers should fall into one of two categories:

-   Regular research papers (12 pages)
-   Extended abstracts (2 pages)

Submission is handled through Easychair:


Regular research papers are expected to present novel and interesting
research results. Extended abstracts should report work in progress that
the authors would like to present at the workshop.

We welcome submissions from PC members (with the exception of the two
co-chairs), but these submissions will be held to a higher standard.

All submissions should be in portable document format (PDF), formatted
using the ACM SIGPLAN style guidelines (two-column, 9pt). Extended
abstracts must be submitted with the label 'Extended abstract' clearly
in the title.

# Important Dates

-   Regular paper deadline: Friday, 10th June, 2016
-   Extended abstract deadline: Friday, 24th June, 2016
-   Author notification: Friday, 8th July, 2016
-   Workshop: Sunday, 18th September, 2016

# Travel Support

Student attendees with accepted papers can apply for a SIGPLAN PAC grant
to help cover travel expenses. PAC also offers other support, such as
for child-care expenses during the meeting or for travel costs for
companions of SIGPLAN members with physical disabilities, as well as for
travel from locations outside of North America and Europe. For details
on the PAC program, see its web page.

Agda mailing list
publicityifl | 24 May 21:13 2016

1st CfP: IFL 2016 (28th Symposium on Implementation and Application of Functional Languages)


Please, find below the first call for papers for IFL 2016.
Please forward these to anyone you think may be interested.
Apologies for any duplicates you may receive.

best regards,
Jurriaan Hage
Publicity Chair of IFL


IFL 2016 - Call for papers


KU Leuven, Belgium

In cooperation with ACM SIGPLAN

August 31 - September 2, 2016



The goal of the IFL symposia is to bring together researchers actively engaged
in the implementation and application of functional and function-based
programming languages. IFL 2016 will be a venue for researchers to present and
discuss new ideas and concepts, work in progress, and publication-ripe results
related to the implementation and application of functional languages and
function-based programming.


Following the IFL tradition, IFL 2016 will use a post-symposium review process
to produce the formal proceedings. All participants of IFL 2016 are invited to
submit either a draft paper or an extended abstract describing work to be
presented at the symposium. At no time may work submitted to IFL be
simultaneously submitted to other venues; submissions must adhere to ACM
SIGPLAN's republication policy:


The submissions will be screened by the program committee chair to make sure
they are within the scope of IFL, and will appear in the draft proceedings
distributed at the symposium. Submissions appearing in the draft proceedings
are not peer-reviewed publications. Hence, publications that appear only in the
draft proceedings are not subject to the ACM SIGPLAN republication policy.
After the symposium, authors will be given the opportunity to incorporate the
feedback from discussions at the symposium and will be invited to submit a
revised full article for the formal review process. From the revised
submissions, the program committee will select papers for the formal
proceedings considering their correctness, novelty, originality, relevance,
significance, and clarity. The formal proceedings will appear in the
International Conference Proceedings Series of the ACM Digital Library.

Important dates

August 1: Submission deadline draft papers
August 3: Notification of acceptance for presentation
August 5: Early registration deadline
August 12: Late registration deadline
August 22: Submission deadline for pre-symposium proceedings
August 31 - September 2: IFL Symposium
December 1: Submission deadline for post-symposium proceedings
January 31, 2017: Notification of acceptance for post-symposium proceedings
March 15, 2017: Camera-ready version for post-symposium proceedings

Submission details

Prospective authors are encouraged to submit papers or extended abstracts to be
published in the draft proceedings and to present them at the symposium. All
contributions must be written in English. Papers must use the new ACM two
columns conference format, which can be found at:


For the pre-symposium proceedings we adopt a 'weak' page limit of 12 pages. For
the post-symposium proceedings the page limit of 12 pages is firm.

Authors submit through EasyChair:



IFL welcomes submissions describing practical and theoretical work as well as
submissions describing applications and tools in the context of functional
programming. If you are not sure whether your work is appropriate for IFL 2016,
please contact the PC chair at tom.schrijvers-4rd9VHyGk8h2kGVRwRwAbw@public.gmane.org. Topics of interest include,
but are not limited to:

- language concepts
- type systems, type checking, type inferencing
- compilation techniques
- staged compilation
- run-time function specialization
- run-time code generation
- partial evaluation
- (abstract) interpretation
- metaprogramming
- generic programming
- automatic program generation
- array processing
- concurrent/parallel programming
- concurrent/parallel program execution
- embedded systems
- web applications
- (embedded) domain specific languages
- security
- novel memory management techniques
- run-time profiling performance measurements
- debugging and tracing
- virtual/abstract machine architectures
- validation, verification of functional programs
- tools and programming techniques
- (industrial) applications

Peter Landin Prize

The Peter Landin Prize is awarded to the best paper presented at the symposium
every year. The honored article is selected by the program committee based on
the submissions received for the formal review process. The prize carries a
cash award equivalent to 150 Euros.

Programme committee

Chair: Tom Schrijvers, KU Leuven, Belgium

- Sandrine Blazy, University of Rennes 1, France
- Laura Castro, University of A Coruña, Spain
- Jacques, Garrigue, Nagoya University, Japan
- Clemens Grelck, University of Amsterdam, The Netherlands
- Zoltan Horvath, Eotvos Lorand University, Hungary
- Jan Martin Jansen, Netherlands Defence Academy, The Netherlands
- Mauro Jaskelioff, CIFASIS/Universidad Nacional de Rosario, Argentina
- Patricia Johann, Appalachian State University, USA
- Wolfram Kahl, McMaster University, Canada
- Pieter Koopman, Radboud University Nijmegen, The Netherlands
- Shin-Cheng Mu, Academia Sinica, Taiwan
- Henrik Nilsson, University of Nottingham, UK
- Nikolaos Papaspyrou, National Technical University of Athens, Greece
- Atze van der Ploeg, Chalmers University of Technology, Sweden
- Matija Pretnar, University of Ljubljana, Slovenia
- Tillmann Rendel, University of Tübingen, Germany
- Christophe Scholliers, Universiteit Gent, Belgium
- Sven-Bodo Scholz, Heriot-Watt University, UK
- Melinda Toth, Eotvos Lorand University, Hungary
- Meng Wang, University of Kent, UK
- Jeremy Yallop, University of Cambridge, UK


The 28th IFL will be held in association with the Faculty of Computer Science,
KU Leuven, Belgium. Leuven is centrally located in Belgium and can be easily
reached from Brussels Airport by train (~15 minutes). The venue in the
Arenberg Castle park can be reached by foot, bus or taxi from the city center.
See the website for more information on the venue.
Agda mailing list
Pierre Hyvernat | 24 May 08:54 2016

PLRR 2017 (Parametricity, Logical Relations & Realizability), call for contribution

                       CALL FOR CONTRIBUTIONS

                         Workshop PLRR 2016
         Parametricity, Logical Relations & Realizability
                  September 2, Marseille, France


                   Satellite workshop - CSL 2016


The workshop PLRR 2016 aims at presenting recent work on parametricity,
logical relations and realizability, and encourage interaction between
those communities.

The areas of interest include, but are not limited to:
* Kleene's intuitionistic realizability,
* Krivine's classical realizability,
* other extensions of the Curry-Howard correspondence,
* links between forcing and the Curry-Howard correspondence,
* parametricity,
* logical relations,
* categorical models,
* applications to programming languages.


Neil Ghani (University of Strathclyde)

Nick Benton (Microsoft Research, Cambridge)


We solicit contributed talks based on extended abstracts of 2 pages.
Submission are handled by easychair:


Submission of abstracts:    June 15, 2016
Notification of acceptance: July  1, 2016


via the main CSL 2016 website: http://csl16.lif.univ-mrs.fr/


Collocated with CSL 2016, hosted by Aix-Marseille Université. Both the
main conference and its satellite workshops will be held in the city
center campus of the Faculty of Science (Central Building).


Pierre     Hyvernat  (Université Savoie Mont Blanc)
Rodolphe   Lepigre   (Université Savoie Mont Blanc)
Alexandre  Miquel    (Universidad de la Republica, Montevideo)
Christophe Raffalli  (Université Savoie Mont Blanc)
Thomas     Streicher (Technische Universitët Darmstadt)


Martin Escardo | 18 May 13:42 2016

unicode input

When I type \MIV I get a bold V, as I should.

But then after type-checking the file with "Load" (Ctrl-C Ctrl-L), I get 
a box with microscopic



When I do "Kill and restart Agda", I see bold V again.

When I cat the file in the command line, I see the bold V and all 
unicode characters as I intend.

So I seem to have the fonts available.

This happens to many other unicode characters, but not all.

My emacs is 24.3.1 under ubuntu 14.04.

Any ideas?

PS 1. This doesn't happen in a laptop running ubuntu 16.06 with emacs 

PS 2. In both machines, when the offending characters are displayed 
correctly, still we have a problem that a blank line is displayed above 
the character's line, and also below.
Shin-Cheng Mu | 18 May 11:14 2016

AoPA -- Algebra of Programming in Agda (updated 2016)

Hi all,

This is a notification that the library Algebra of Programming
in Agda (AoPA) has been updated and now works with Agda 2.5.1.

AoPA allows one to encode Algebra of Programming (BdM97) style 
program derivation, both functional and relational, in Agda.

New additions include the use of universe polymorphism, 
generic datatypes with polymorphic base functors, and theories 
for developing algorithms from Galois connections (MO11, CM15). 

Development of AoPA is still being continued. For more info,
see the Git Repository:



The program derivation community has been exploring a relational 
theory of program calculation. A problem is specified as a relation 
that maps inputs to outputs, which allows us not to be over 
specific about which output to choose when they are equally good, 
leaving the choices to implementations. The task is to refine the 
specification into a functional implementation, using algebraic 

AoPA allows us to to develop relational proofs, in Agda, in the 
style of Bird and de Moor. Elements of the relational theory of 
programs are modelled in the type system of Agda. Calculations 
are expressed as program terms that, if type-checked, is guaranteed 
to be correct. In the end of a calculation one may extract a 
functional program that is proved to respect the relational 


(BdM97) Richard Bird and Oege de Moor, Algebra of Programming. 
Prentice Hall, 1997.

(MO11) Shin-Cheng Mu and José Nuno Oliveira, Programming from 
Galois connections. The Journal of Logic and Algebraic Programming, 
Volume 81, Issue 6, August 2012, pp 680–704. doi>10.1016/j.jlap.2012.05.003.

(CM15) Yu-Hsi Chiang and Shin-Cheng Mu, Formal derivation of 
greedy algorithms from relational specifications: A tutorial. 
Journal of Logical and Algebraic Methods in Programming. In Press.
Sergei Meshveliani | 17 May 19:42 2016

stuck with "unsolved metas"

Dear Agda developers,

I observe the following effect (in Agad 2.5.1, ghc-7.10.2).

module _ {α α=} (upIR : UpIntegralRing α α=)
         (_∣?_ : let Mg = UpIntegralRing.*magma upIR
                 in  Decidable₂ $ Magma._∣_ Mg
         (open OverIntegralRing-2 upIR _∣?_ using (Prime∣split))
         (prime∣split : Prime∣split)
  open OverIntegralRing-0 upIR _∣?_ using (_∣'?_; *upCMon-NZ; 
  open OverIntegralRing-2 upIR _∣?_ using (Prime∣split←→Prime∣split-nz)

  module NZ =  OfCancellativeCommMonoid-0 *upCMon-NZ *cancel-nz _∣'?_

  implic :  Prime∣split → NZ.Prime∣split
  implic =  proj₁ Prime∣split←→Prime∣split-nz

  debug :  NZ.Prime∣split
  debug =  implic prime∣split

It reports  "unsolved metas"  for the last line.

Usually it helps adding implicit arguments. But not in this case:

    debug =  implic (\ {p a b} → prime∣split {p} {a} {b})

still leads to "unsolved metas" for this line.

Prime∣split  is declared in the two parameterized modules:

OverIntegralRing-2.Prime∣split =
                   ∀ {p a b} → IsPrime p → p ∣ (a * b) → p ∣ a ⊎ p ∣ b

NZ.Prime∣split =   ∀ {p a b} → IsPrime p → p ∣ (a ∙ b) → p ∣ a ⊎ p ∣ b

(IsPrime  is defined a bit differently in the second module, and _*_ is
replaced  _∙_).

These types are type-checked in the `implic' function.
But applying implic to a module parameter value is not type-checked.

Can you, please, advise?
May be, you can somehow guess. 

(The code is large. Many parameterized modules importing each other,
nested records, etc. Difficult to reduce.


Harley Eades III | 10 May 19:26 2016

Not Unfolding Local Defs

Hi, everyone.

I am using a ton of records in my formalization, and at the top of
each module I give several convince definitions for the projections
of my records to make types easier to read.

For example, see the top of this file:


A typical example is the following:

_≤M_ : M → M → Set
_≤M_ = (rel (poset (oncMonoid bp-pf)))

This definition makes reading types a lot easier, but this definition is unfolded
in goals, which makes the goal very hard to read.  Multiply this with a number 
of definitions like this, and we get goals that are close to impossible to read.

So I spend a lot of time trying to parse a goal myself to be able to do the proof.

Is there a way to tell Agda not to unfold these definitions in goals?

Simon Thompson | 10 May 17:35 2016

Trustworthy Refactoring project: Research Associate Positions in Refactoring Functional Programs and Formal Verification (for CakeML)

Trustworthy Refactoring project: Research Associate Positions in Refactoring Functional Programs and
Formal Verification (for CakeML) 

The Trustworthy Refactoring project at the University of Kent is seeking to recruit postdoc research
associates for two 3.5 year positions, to start in September this year.

The overall goal of this project is to make a step change in the practice of refactoring by designing and
constructing of trustworthy refactoring tools. By this we mean that when refactorings are performed,
the tools will provide strong evidence that the refactoring has not changed the behaviour of the code,
built on a solid theoretical understanding of the semantics of the language. Our approach will provide
different levels of assurance from the (strongest) case of a fully formal proof that a refactoring can be
trusted to work on all programs, given some pre-conditions, to other, more generally applicable
guarantees, that a refactoring applied to a particular program does not change the behaviour of that

The project will make both theoretical and practical advances. We will build a fully-verified
refactoring tool for a relatively simple, but full featured programming language (CakeML
https://cakeml.org), and at the other we will build an industrial-strength refactoring tool for a
related industrially-relevant language (OCaml). This OCaml tool will allow us to explore a range of
verification techniques, both fully and partially automated, and will set a new benchmark for building
refactoring tools for programming languages in general. 

The project, which is coordinated by Prof Simon Thompson and Dr Scott Owens, will support two research
associates, and the four will work as a team. One post will focus on pushing the boundaries of trustworthy
refactoring via mechanised proof for refactorings in CakeML, and the other post will concentrate on
building an industrial strength refactoring tool for OCaml. The project has industrial support from
Jane Street Capital, who will contribute not only ideas to the project but also host the second RA for a
period working in their London office, understanding the OCaml infrastructure and their refactoring requirements.

You are encouraged to contact either of the project investigators by email
s.j.thompson@...) if you have any further questions about the
post, or if you would like a copy of the full research application for the project. We expect that
applicants will have PhD degree in computer science (or a related discipline) or be close to completing
one. For both posts we expect that applicants will have experience of writing functional programs, and
for the verification post we also expect experience of developing (informal) proofs in a mathematical or
programming context.

To apply, please go to the following web pages:

Research Associate in Formal Verification for CakeML (STM0682): 


Research Associate in Refactoring Functional Programs (STM0683): 


Simon and Scott

Simon Thompson | Professor of Logic and Computation 
School of Computing | University of Kent | Canterbury, CT2 7NF, UK
s.j.thompson@... | M +44 7986 085754 | W www.cs.kent.ac.uk/~sjt
Serge Leblanc | 9 May 12:48 2016

Stranga konduto !

Kial mi bezonas kazstudadon ĉe 'x' kvankam mi antaŭe indikis la egalecon 'diag x (suc y) = suc (diag (suc x) y)'?
Plie, la erara mesago kontraŭdiras mian difinon de 'diag x (suc y)'?

Why I need a case study on 'x' though I have previously pointed out the equality of 'diag x (suc y) = suc (diag (suc x), y)'?
Moreover, the error message contradicts my definition of 'diag x (suc y)'?

diag x (suc y) != suc (diag (suc x) y) of type ℕ
when checking that the expression refl has type
diag x (suc y) ≡ suc (diag (suc x) y)

Serge Leblanc gpg --keyserver hkp://keyserver.ubuntu.com:11371 --recv-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
module Test where

open import Data.Nat using (ℕ ; zero ; suc ; _+_)
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_ ; refl ; sym ; cong ) 

diag : ℕ → ℕ → ℕ
diag zero zero = zero
diag (suc x) zero = suc (x + diag x zero)
diag x (suc y) = suc (diag (suc x) y)

diag≡ : ∀ x y → diag x (suc y) ≡ suc (diag (suc x) y)
diag≡ x y = refl

diag≡′ : ∀ x y → diag x (suc y) ≡ suc (diag (suc x) y)
diag≡′ zero y = refl
diag≡′ (suc x) y = refl
Agda mailing list
Serge Autexier | 4 May 17:38 2016

Last Call for Papers: Workshop on User Interfaces for Theorem Provers (UITP 2016 <at> IJCAR), Coimbra, Portugal, Deadline May 17th *NEW* (was May 9th, 2016)

                         Last Call for Papers

                              UITP 2016
  12th International Workshop on User Interfaces for Theorem Provers
                    in connection with IJCAR 2016
                  July 2nd, 2016, Coimbra, Portugal

              * NEW Submission deadline: May 17th, 2016 *

- Invited Speaker: Sylvain Conchon (LRI, France) giving a talk about
  "AltGr-Ergo, a graphical user interface for the SMT solver Alt-Ergo"
- Submission deadline postponed by one week to May, 17th, 2016

The  User  Interfaces  for  Theorem  Provers  workshop  series  brings
together   researchers  interested   in   designing,  developing   and
evaluating interfaces  for interactive proof systems,  such as theorem
provers,  formal  method  tools,  and  other  tools  manipulating  and
presenting mathematical formulas.

While  the reasoning  capabilities of  interactive proof  systems have
increased dramatically over the last years, the system interfaces have
often  not   enjoyed  the   same  attention   as  the   proof  engines
themselves.  In many  cases,  interfaces remain  relatively basic  and

The User  Interfaces for  Theorem Provers  workshop series  provides a
forum for  researchers interested in improving  human interaction with
proof  systems. We  welcome participation  and contributions  from the
theorem proving, formal  methods and tools, and  HCI communities, both
to  report on  experience with  existing systems,  and to  discuss new
directions. Topics covered include, but are not limited to:

- Application-specific  interaction mechanisms  or designs  for prover
  interfaces Experiments and evaluation of prover interfaces
- Languages and tools for authoring, exchanging and presenting proof
- Implementation  techniques (e.g.  web  services, custom  middleware,
- Integration of interfaces and tools to explore and construct proof
- Representation and manipulation of mathematical knowledge or objects
- Visualisation of mathematical objects and proof
- System descriptions

UITP 2016 is a one-day workshop to be held on Saturday, July 2nd, 2016
in Coimbra, Portugal, as a IJCAR 2016 workshop.

** Submissions **

Submitted   papers  should   describe   previously  unpublished   work
(completed or  in progress), and  be at least 4  pages and at  most 12
pages. We encourage concise and relevant papers. Submissions should be
in PDF format, and typeset with  the EPTCS LaTeX document class (which
can be downloaded from  http://style.eptcs.org/). Submission should be
done via EasyChair at 


All papers will be peer reviewed by members of the programme committee
and selected by the organizers in accordance with the referee

At  least one  author/presenter  of accepted  papers  must attend  the
workshop and present their work.

** Proceedings **

Authors will have the opportunity to incorporate feedback and insights
gathered during the  workshop to improve their  accepted papers before
publication  in the  Electronic  Proceedings  in Theoretical  Computer
Science (EPTCS - http://www.eptcs.org/).

** Important dates **

 Submission deadline: May 17th, 2016
 Acceptance notification: June 6th, 2016
 Camera-ready copy: June 20th, 2016
 Workshop: July 2nd, 2016

** Programme Committee **

 Serge Autexier, DFKI Bremen, Germany (Co-Chair)
 Pedro Quaresma, U Coimbra, Portugal (Co-Chair)
 David Aspinall, University of Edinburgh, Scotland
 Chris Benzmüller, FU Berlin, Germany & Stanford, USA
 Yves Bertot, INRIA Sophia-Antipolis, France
 Gudmund Grov, Heriott-Watt University, Scotland
 Zoltán Kovács, RISC, Austria
 Christoph Lüth, University of Bremen and DFKI Bremen, Germany
 Alexander Lyaletski, Kiev National Taras Shevchenko Univ., Ukraine
 Michael Norrish, NICTA, Australia
 Andrei Paskevich, LRI, France
 Christian Sternagel, University Innsbruck, Austria
 Enrico Tassi, INRIA Sophia-Antipolis, France
 Laurent Théry, INRIA Sophia-Antipolis, France
 Makarius Wenzel, Sketis, Germany
 Wolfgang Windsteiger, RISC Linz, Austria
 Bruno Woltzenlogel Paleo, TU Vienna, Austria
Nils Anders Danielsson | 4 May 15:19 2016

Add Agda papers to the wiki


Have you written any paper that uses Agda in some way (in the text or in
an accompanying formalisation), but is not listed on the following Agda
Wiki page?


In that case, please list the paper. The wiki can be edited without
registration. If you don't feel like editing the wiki yourself you can
also send the information to me.

Our group in Gothenburg will soon apply for money to (among other
things) continue developing Agda, and one way to indicate that Agda is
useful to our community is to show that Agda is used to produce papers.