Andrés Sicard-Ramírez | 30 Mar 17:37 2015

Poll: Remove the Epic back-end


At the moment, Epic ( and the
Epic back-end are unmaintained. We might consider to remove the Epic

If you are using the Epic back-end, please reply this message.



Sergei Meshveliani | 30 Mar 16:43 2015

type check performance

Dear Agda developers.

I have a certain middle-size project, call it "FooLib library".
I am going to publish it soon, but first it would have sense to try to 
reduce its space eagerness.
And I wonder how to reduce.

Its type check in  Agda  takes

    9G byte memory and  10 minutes  (on a 2 GHz machine),

    the further compilation (by MAlonzo, ghc-7.8.3 etc.) takes  
                                                         37 minutes.

Then, after all the FooLib is compiled,
type check and compilation of a small Main module 
(which imports almost all modules of Foo) takes  
                      10 minutes  and again,  9 Gb memory.

Please, how to reduce this  9 Gb requirement?

I know about the possibilities of 
1) with --> case,
2) using `private' for some proof pieces.
Also the project meaning is so that `private' has sense to apply to 
almost all proofs in FooLib, and this makes it more than 9/10 of the

1) with --> case  is often difficult to arrange,
(Continue reading)

Stephanie Weirich | 27 Mar 22:00 2015

Mentoring workshop <at> ICFP

CALL for Applications for Student Travel Support

SIGPLAN Programming Languages Mentoring Workshop  <at>  ICFP
Vancouver, BC (co-located with ICFP 2015)
Sunday, August 30th, 2015

We are pleased to invite students interested in functional programming research to the programming
languages mentoring workshop at ICFP. The goal of this workshop is to introduce senior undergraduate and
early graduate students to research topics in functional programming as well as provide career
mentoring advice to help them get through graduate school, land a great job, and succeed. We have
recruited leaders from the functional programming community to provide overviews of current research
topics, and give
students valuable advice about how to thrive in graduate school, search for a job, and cultivate habits and
skills that will help them in research careers.

This workshop is part of the activities surrounding ICFP, the International Conference on Functional
Programming, and takes place the day before the main conference. One goal of the workshop is to make the
ICFP conference more accessible to newcomers and we hope that participants will stay through the entire conference.

Through the generous donation of our sponsors, we are able to provide travel scholarships to fund student
participation. These travel scholarships will cover reasonable travel expenses (airfare, hotel and
registration fees) for attendance at both the workshop and the ICFP
conference. Anyone may apply for a travel scholarship, but first priority will be given to women and
underrepresented minority applicants from the United States and Canada.

The workshop is open to all. Students with alternative sources of funding for their travel and
registration fees are welcome. In particular, many student attendance programs provide full or partial
travel funding for students to attend ICFP 2015, including the ACM Student Research Competition. More
(Continue reading)

Sergei Meshveliani | 24 Mar 11:29 2015

fast DecTotalOrder

Can people, please, advise me on the following matter?
(which is in fact on Standard library)

For testing the sorting function for performance, I need 
(1) the list elements to be from some DecTotalOrder instance
     (required by the `sort' function),
(2) _≤?_ to perform fast,
(3) forming a list having as many different elements as needed.

I am going to do this.

a) To implement  
   stoToDTO : StrictTotalOrder _ _ _→ DecTotalOrder _ _ _
   stoToDTO sto =
                 record{ Carrier = Carrier
                       ; _≈_     = _≈_
                       ; _≤_     = _≤_
                       ; isDecTotalOrder = isDecTotalOrder }
   open StrictTotalOrder sto using (_≈_; _<_; compare ...)

   _≤_ : Rel Carrier _
   x ≤ y =  x < y ⊎ x ≈ y   -- **

I expect that  DecTotalOrder  can be proved for this _≤_ instance.

b) To use  Data.String.StrictTotalOrder,
   in which  _<_  is by the lexicographic comparison.
(Continue reading)

Sergei Meshveliani | 22 Mar 13:39 2015

+-mono arguments

Who knows, please, 
is it possible to cancel below explicit signatures for  1≤sm  and  sm≤sm
and to use their values directly as arguments for  _+-mono_

(see attachment)



  aux : (m n : ℕ) → m + m ≡ 2 + n → m < 2 + n 
  aux 0 _     ()  
  aux (suc m) n  sm+sm≡2+n  with  (2 + m) ≤? (2 + n)
  ... | yes res     = res
  ... | no  ssm≰2+n = ⊥-elim $ sm+sm≢2+n sm+sm≡2+n
                sm = suc m 

                2+n<ssm = ≰→> ssm≰2+n 
                sn≤m    = pred-mono $ pred-mono 2+n<ssm

                1≤sm : 1 ≤ sm
                1≤sm = s≤s z≤n

                sm≤sm : sm ≤ sm 
                sm≤sm = ≤refl PE.refl  
(Continue reading)

Faruk Caglar | 20 Mar 17:04 2015


[Apologies if you receive multiple copies of this email]

                    ACM SIGPLAN GPCE 2015
              14th International Conference on
        Generative Programming: Concepts & Experiences

             Oct 26-27, 2015, Pittsburgh, PA, USA

Co-located with:
ACM SIGPLAN conference on Systems, Programming, Languages and
Applications: Software for Humanity (SPLASH 2015)
ACM SIGPLAN 8th International Conference on Software Language
Engineering (SLE) 2015


  Abstract submission   : June 8, 2015
  Full paper submission : June 15, 2015
  Authors notification  : July 24, 2015
  Camera-ready          : Aug 7, 2015
  Conference            : Oct 26-27, 2015

  Workshops: Handled by SPLASH

All dates are Anywhere on Earth


GPCE is a venue for researchers and practitioners interested in techniques
that use program generation, domain-specific languages, and component
deployment to increase programmer productivity, improve software quality,
and shorten the time-to-market of software products. In addition to
exploring cutting-edge techniques of generative software, our goal is to
foster further cross-fertilization between the software engineering and the
programming languages research communities.


GPCE seeks contributions on all topics related to generative software and
its properties. Topics of interest include, but are not limited to:

Generative software
* Domain-specific languages (language extension, language embedding,
  language design, language theory, language workbenches, interpreters,
* Product lines (domain engineering, feature-oriented and
  aspect-oriented programming, pre-processors, feature interactions)
* Metaprogramming (reflection, staging, partial evaluation), Type
  systems, Program synthesis
* Implementation techniques and tool support (components, plug-ins,
  libraries, metaprogramming, macros, templates, generic programming,
  run-time code generation, model-driven development, composition tools,
  code-completion and code-recommendation systems)

Practical Applications and Empirical evaluations
* Empirical evaluations of all topics above (user studies, substantial case
  studies, controlled experiments, surveys, rigorous measurements) 
* Application areas and engineering practice (Cloud Computing, Internet of
  Things, Cyber Physical Systems, Mobile Computing, Software Defined
  Networking, High Performance Computing, Patterns and Middleware,
  Development methods)

Properties of generative software
* Correctness of generators and generated code (analysis, testing, formal
  methods, domain-specific error messages, safety, security)  
* Reuse and evolution
* Modularity, separation of concerns, understandability, and
* Performance engineering, nonfunctional properties (program optimization
  and parallelization, GPGPUs, multicore, footprint, metrics)

We particularly welcome papers that address some of the key challenges in
the field, such as,
* synthesizing code from declarative specifications
* supporting extensible languages and language embedding
* ensuring correctness and other nonfunctional properties of generated code
* proving generators correct
* improving error reporting with domain-specific error messages
* reasoning about generators
* handling variability-induced complexity in product lines
* providing efficient interpreters and execution languages
* human factors in developing and maintaining generators

GPCE encourages submissions about empirical evaluations and applications of
generative software, and such papers will be given special consideration
during reviewing.


Research papers: 10 pages maximum (ACM SIGPLAN style)

Research papers should report on original and unpublished results of
theoretical, empirical, conceptual, or experimental research that
contribute to scientific knowledge in the areas listed above (the PC chair
can advise on appropriateness)

Tool demos and short papers: 4 pages maximum (ACM SIGPLAN style).

The goal of short papers is to promote current work on research and
practice. Short papers represent an early communication of research and do
not always require complete results as in the case of a full paper. In this
way, authors can introduce new ideas to the community, discuss ideas and
get early feedback. Please note that short papers are not intended to be
position statements. Short papers are included in the proceedings and will
be presented with a shorter time slot at the conference.

Tool demonstrations should present tools that implement generative
techniques, and are available for use. Any of the GPCE topics of interest
are appropriate areas for tool demonstrations, although purely commercial
tool demonstrations will not be accepted. Submissions must provide a tool
description of 4 pages in SIGPLAN proceedings style (see above) and a
demonstration outline including screenshots of up to 4 pages. Tool
demonstrations must have the words "Tool Demo" or "Tool Demonstration" in
the title, possibly appended in parenthesis. The 4-page tool description
will, if the demonstration is accepted, be published in the proceedings.



  Christian Kastner, Carnegie Mellon University, Pittsburgh, PA, USA


  Aniruddha Gokhale, Vanderbilt University, Nashville, TN, USA


  Faruk Caglar, Vanderbilt University, Nashville, TN, USA
  Tomofumi Yuki, INRIA Rhone-Alpes, France


  Kenichi Asai, Ochanomizu Univ, Japan
  Emilie Balland, INRIA Bordeaux, France
  Don Batory, Univ of Texas, USA
  Walter Binder, Univ of Lugano, Switzerland
  Jan Bosch, Chalmers Univ, Sweden
  Akshay Dabholkar, Oracle, USA
  Ewen Denney, NASA Ames, USA
  Katrina Falkner, Univ of Adelaide, Australia
  Bernd Fischer, Stellenbosch Univ, South Africa
  Matthew Flatt, Univ of Utah, USA
  Jeff Gray, Univ of Alabama, USA
  Michael Haupt, Oracle Labs, Germany
  James Hill, Indiana Univ Purdue Univ at Indianapolis, USA
  Young-Woo Kwon, Utah State Univ, USA
  Raffaela Mirandola, Politechnico di Milano, Italy
  Hridesh Rajan, Iowa State Univ, USA
  Laurent Reveillere, LaBRI, Univ of Bordeaux, France
  Marcio Ribeiro, Federal Univ of Alagoas, Brazil
  Tiark Rompf, Purdue Univ, USA
  Klaus Schmid, Stiftung Universitat Hildesheim, Germany
  Norbert Siegmund, Univ of Passau, Germany
  Yannis Smaragdakis, Univ of Athens, Greece
  Sumant Tambe, RTI Inc, USA
  Petr Tuma, Charles Univ, Czech Republic
  Nalini Venkatasubramanian, Univ of California, Irvine, USA
  Jules White, Vanderbilt Univ, USA
  Eric Wohlstadter, Univ of British Columbia, Canada

Agda mailing list
Peter Achten | 18 Mar 10:47 2015

[TFP'15] final call for papers - extended deadline march 31 -

                     L A S T    A L L   F O R   P A P E R S

                         ======== TFP 2015 ===========

               16th Symposium on Trends in Functional Programming
                                June 3-5, 2015
                        Inria Sophia Antipolis, France

The symposium on Trends in Functional Programming (TFP) is an
international forum for researchers with interests in all aspects of
functional programming, taking a broad view of current and future
trends in the area. It aspires to be a lively environment for
presenting the latest research results, and other contributions (see
below). Authors of draft papers will be invited to submit revised
papers based on the feedback receive at the symposium.  A
post-symposium refereeing process will then select a subset of these
articles for formal publication.

The selected revised papers will be published as a Springer Lecture
Notes in Computer Science ( volume.

TFP 2015 will be the main event of a pair of functional programming
events. TFP 2015 will be accompanied by the International Workshop on
Trends in Functional Programming in Education (TFPIE), which will take
place on June 2nd.

The TFP symposium is the heir of the successful series of Scottish
Functional Programming Workshops. Previous TFP symposia were held in
   * Edinburgh (Scotland) in 2003;
   * Munich (Germany) in 2004;
   * Tallinn (Estonia) in 2005;
   * Nottingham (UK) in 2006;
   * New York (USA) in 2007;
   * Nijmegen (The Netherlands) in 2008;
   * Komarno (Slovakia) in 2009;
   * Oklahoma (USA) in 2010;
   * Madrid (Spain) in 2011;
   * St. Andrews (UK) in 2012;
   * Provo (Utah, USA) in 2013;
   * and in Soesterberg (The Netherlands) in 2014.
For further general information about TFP please see the TFP homepage.


TFP is pleased to announce talks by the following two invited speakers:

   * Laurence Rideau is a researcher at INRIA and is interested in the
     semantics of programming languages , the formal methods, and the
     verification tools for programs and mathematical proofs.  She
     participated in the beginnings of the Compcert project (certified
     compiler), and is part of the Component Mathematical team in the
     MSR-INRIA joint laboratory, who performed the formalization of the
     Feit-Thompson theorem successfully.

     Thirty years ago, computers barged in mathematics with the famous
     proof of the Four Color Theorem.  Initially limited to simple
     calculation, their role is now expanding to the reasoning whose
     complexity is beyond the capabilities of most humans, as the proof of
     the classification of finite simple groups.  We present our large
     collaborative adventure around the formalization of the Feit-Thompson
     theorem (
     that is a first step to the classification of finite groups
     and that uses a palette of methods and techniques that range from
     formal logic to software (and mathematics) engineering.

   * Anil Madhavapeddy

== SCOPE ==

The symposium recognizes that new trends may arise through various
routes.  As part of the Symposium's focus on trends we therefore
identify the following five article categories. High-quality articles
are solicited in any of these categories:

     Research Articles: leading-edge, previously unpublished research work
     Position Articles: on what new trends should or should not be
     Project Articles: descriptions of recently started new projects
     Evaluation Articles: what lessons can be drawn from a finished project
     Overview Articles: summarizing work with respect to a trendy subject

Articles must be original and not simultaneously submitted for
publication to any other forum. They may consider any aspect of
functional programming: theoretical, implementation-oriented, or
experience-oriented.  Applications of functional programming
techniques to other languages are also within the scope of the

Topics suitable for the symposium include:

     Functional programming and multicore/manycore computing
     Functional programming in the cloud
     High performance functional computing
     Extra-functional (behavioural) properties of functional programs
     Dependently typed functional programming
     Validation and verification of functional programs
     Debugging and profiling for functional languages
     Functional programming in different application areas:
       security, mobility, telecommunications applications, embedded 
       global computing, grids, etc.
     Interoperability with imperative programming languages
     Novel memory management techniques
     Program analysis and transformation techniques
     Empirical performance studies
     Abstract/virtual machines and compilers for functional languages
     (Embedded) domain specific languages
     New implementation strategies
     Any new emerging trend in the functional programming area

If you are in doubt on whether your article is within the scope of
TFP, please contact the TFP 2015 program chair, Manuel Serrano.


To reward excellent contributions, TFP awards a prize for the best paper
accepted for the formal proceedings.

TFP traditionally pays special attention to research students,
acknowledging that students are almost by definition part of new
subject trends. A student paper is one for which the authors state
that the paper is mainly the work of students, the students are listed
as first authors, and a student would present the paper. A prize for
the best student paper is awarded each year.

In both cases, it is the PC of TFP that awards the prize.  In case the
best paper happens to be a student paper, that paper will then receive
both prizes.


TFP is financially supported by Erlang Solutions.


Acceptance of articles for presentation at the symposium is based on a
lightweight peer review process of extended abstracts (4 to 10 pages
in length) or full papers (20 pages). The submission must clearly
indicate which category it belongs to: research, position, project,
evaluation, or overview paper. It should also indicate which authors
are research students, and whether the main author(s) are students.  A
draft paper for which ALL authors are students will receive additional
feedback by one of the PC members shortly after the symposium has
taken place.

We use EasyChair for the refereeing process. Papers must be submitted at:

Papers must be written in English, and written using the LNCS
style. For more information about formatting please consult the
Springer LNCS web site:


Submission of draft papers:     March 31, 2015
Notification:                   April 7, 2015
Registration:                   May 4, 2015
TFP Symposium:                  June 3-5, 2015
Student papers feedback:        June 9, 2015
Submission for formal review:   July 1, 2015
Notification of acceptance:     September 8, 2015
Camera ready paper:             October 8, 2015


Janis Voigtländer               University of Bonn, DE
Scott Owens                     University of Kent, UK
Neil Sculthorpe                 Swansea University, UK
Colin Runciman                  University of York, UK
Manuel Serrano                  Inria (PC chair), FR
Rinus Plasmeijer                University of Nijmegen, NL
Tomas Petricek                  University of Cambridge, UK
Marco T. Morazan                Seton Hall University, USA
Wolfgang De Meuter              Vrije Universiteit Brussel, BE
Michel Mauny                    Ensta ParisTech, FR
Sam Lindley                     The University of Edinburgh, UK
Daan Leijen                     Microsoft, USA
Jurriaan Hage                   Utrecht University, NL
Andy Gill                       University of Kansas, USA
Thomas Gazagnaire               University of Cambrige, UK
Lars-Ake Fredlund               Universidad Politécnica de Madrid, ES
Jean-Christophe Filliatre       Université Paris Sud Orsay, FR
Marc Feeley                     Université de Montréal, CA
Olaf Chitil                     University of Kent, UK
Edwin Brady                     University of St Andrews, UK
Sergei Meshveliani | 17 Mar 13:44 2015

Decidable _\equiv_


I have the two questions on the declaration of

  module Foo {α α= α≤} 
             (dto  : DecTotalOrder α α= α≤)
             (_≡?_ : Decidable (_≡_ {A = DecTotalOrder.Carrier dto})))

1. Is it possible here something like 
                  (_≡?_ : let C = DecTotalOrder.Carrier dto
                          in  Decidable (_≡_ {A = C})

2. (As  dto  implies  Decidable _≈_),
   can this  _≡?_  be derived from  dto ?

   (I suspect that it cannot).


Tarmo Uustalu | 15 Mar 22:17 2015

TYPES 2015 submission deadline extended

[Submission deadline extended by a week to 20 March 2015.
Consider contributing!]

                      CALL FOR CONTRIBUTIONS

   21st International Conference on Types for Proofs and Programs,
                            TYPES 2015
                 Tallinn, Estonia,  18-21 May 2015



The TYPES meetings are a forum to present new and on-going work in all
aspects of type theory and its applications, especially in formalized
and computer assisted reasoning and computer programming. The meetings
from 1990 to 2008 were annual workshops of a sequence of five EU
funded networking projects. Since 2009, TYPES has been run as an
independent conference series. Previous TYPES meetings were held in
Antibes (1990), Edinburgh (1991), Båstad (1992), Nijmegen (1993),
Båstad (1994), Torino (1995), Aussois (1996), Kloster Irsee (1998),
Lökeberg (1999), Durham (2000), Berg en Dal near Nijmegen (2002),
Torino (2003), Jouy en Josas near Paris (2004), Nottingham (2006),
Cividale del Friuli (2007), Torino (2008), Aussois (2009), Warsaw
(2010), Bergen (2011), Toulouse (2013), Paris (2014).

The TYPES areas of interest include, but are not limited to:

    foundations of type theory and constructive mathematics;
    applications of type theory;
    dependently typed programming;
    industrial uses of type theory technology;
    meta-theoretic studies of type systems;
    proof assistants and proof technology;
    automation in computer-assisted reasoning;
    links between type theory and functional programming;
    formalizing mathematics using type theory.

We encourage talks proposing new ways of applying type theory.

Invited speakers

Gilles Barthe (IMDEA Software)
Andrej Bauer (University of Ljubljana)
Peter Selinger (Dalhousie University)


Joachim Kock (Universitat Autònoma de Barcelona)
Peter LeFanu Lumsdaine (Stockholm University) 

Contributed talks

We solicit contributed talks. Selection of those will be based on
extended abstracts/short papers of 2 pp formatted with
easychair.cls. Submission is via EasyChair by 20 March 2015. The
authors will be notified of acceptance/rejection by 10 April 2015.

Camera-ready versions of the accepted contributions, due by 1 May
2015, will be published in an informal book of abstracts for
distribution at the workshop.


Similarly to TYPES 2011, 2013, 2014, we will publish a
post-proceedings in the Leibniz International Proceedings in
Informatics (LIPIcs) series. Submission to that volume will be open
for everyone. Tentative submission deadline: mid-September 2015.

Programme committee

Andrea Asperti (Università di Bologna)
Robert Atkey (University of Edinburgh)
Ulrich Berger (Swansea University)
Jean-Philippe Bernardy (Chalmers University of Technology)
Edwin Brady (University of St Andrews)
Joëlle Despeyroux (INRIA Sophia Antipolis - Méditerranée)
Herman Geuvers (Radboud Universiteit Nijmegen)
Sam Lindley (University of Edinburgh)
Assia Mahboubi (INRIA Saclay - Île-de-France)
Ralph Matthes (IRIT, CNRS and Université Paul Sabatier)
Aleksandar Nanevski (IMDEA Software)
Christine Paulin-Mohring (LRI, Université Paris-Sud)
Simona Ronchi Della Rocca (Università di Torino)
Ulrich Schöpp (Ludwig-Maximilians-Universität München)
Bas Spitters (Carnegie Mellon University)
Pawel Urzyczyn (University of Warsaw)
Tarmo Uustalu (Institute of Cybernetics, Tallinn) (chair)


Logic and semantics group, Institute of Cybernetics, Tallinn


ERDF via EXCS, the Estonian Centre of Excellence in Computer Science
Sergei Meshveliani | 15 Mar 22:07 2015

unused values

Dear Agda developers,

It will be extremely useful to have the type checker warnings 
(switched by the option) for

   unused values (types), unused import, and such
   (like it is in Glasgow Haskell).


Conor McBride | 13 Mar 12:51 2015

Help, I'm failing at sized types.


Sorry to be a nuisance.

I’m trying to do some stuff with sized types, but I think I’m failing at basic stuff like finding
the on-switch. Specifically…

{-# OPTIONS --sized-types #-}

module SizeFail where

open import Agda.Primitive
  Size : Set
  Size<_ : Size -> Set
  up : Size -> Size
  infty : Size
{-# BUILTIN SIZE Size #-}
{-# BUILTIN SIZELT Size<_ #-}
{-# BUILTIN SIZEINF infty #-}

data Foo : Size -> Set where
  boo : {i : Size} -> Foo i
  coo : {i : Size} -> Foo i -> Foo (up i)

subtype? : {i : Size} -> Foo i -> Foo infty
subtype? t = t

…results in the complaint...

.i != infty of type Size
when checking that the expression t has type Foo infty

…whether the pragmas are present or not.

Any light gratefully received.

(Longer term, I want to do some syntactic mangling in which renaming is obviously size-preserving, so I can
apply a renaming to a substructure before I do a recursive call on it.)