publicityifl | 2 Sep 09:23 2014

Third call for papers, IFL 2014


Please, find below the third call for papers for IFL 2014.
The submission page is now open. The submission date has been
delayed to Sep. 8 2014 anywhere on the world.

Please forward these to anyone you think may be interested.
Apologies for any duplicates you may receive.

best regards,
Jurriaan Hage





OCTOBER 1-3, 2014

We are pleased to announce that the 26th edition of the IFL series
will be held at Northeastern University in Boston, USA. The symposium
will be held from 1st to 3rd of October 2014.

(Continue reading)

Sergei Meshveliani | 31 Aug 17:00 2014

foo ∘ fromFoo strangeness

I observe the program 

open import Function using (id; _∘_)
open import Relation.Binary.PropositionalEquality as PE using (_≗_)

module _ α (A : Set α)
  data Foo : Set α  where  foo : A → Foo

  fromFoo : Foo → A
  fromFoo (foo x) = x

  fromFoo∘foo : fromFoo ∘ foo ≗ id
  fromFoo∘foo _ = PE.refl

  foo∘fromFoo : foo ∘ fromFoo ≗ id
  foo∘fromFoo _ =  PE.refl {A = Foo}

fromFoo∘foo  is type-checked (in Agda-2.4.2).

For  foo∘fromFoo,  
I expected that if it is not type-checked, it would report of 
"unsolved metas".
But it reports     " foo (fromFoo .x) != .x of type Foo  ... "

Anyway, the thing can be implemented by 
foo∘fromFoo (foo _) =  PE.refl 
(Continue reading)

Hugo Herbelin | 29 Aug 17:37 2014

Final CFP Post-proceedings TYPES 2014 Types for Proofs and Programs (open call, extended deadline)

 Final call for papers: Types for Proofs and Programs,
      post-proceedings of TYPES 2014 (open call)     
(with deadline extension and corrected submission link)

TYPES is a major forum for the presentation of research on all aspects
of type theory and its applications. The post-proceedings of TYPES
2014, which was held May 12-15 in Paris, are open to everyone, also
those who did not participate in the conference. We would like to
invite all researchers that study type systems to share their results
concerning type-based theorem proving environments or type-based
formal modelling, in particular we welcome submissions on any topic in
the following list:

 - 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
 - Formalising mathematics using type theory. 

Important dates

Abstract submission deadline:   8 September 2014 (new deadline)
Paper submission deadline:     15 September 2014 (new deadline)
Notification of acceptance:    15 February  2015
(Continue reading)

Andrés Sicard-Ramírez | 29 Aug 15:23 2014

ANNOUNCE: Standard library version 0.8.1


Standard library 0.8.1 has been released (see

The library has been tested using Agda 2.4.2.

Changes since 0.8:

Note that no guarantees are made about backwards or forwards
compatibility, the library is still at an experimental stage.

If you want to compile the library using the MAlonzo compiler, then
you should first install some supporting Haskell code, for instance as

  cd ffi
  cabal install

Currently the library does not support the Epic or JavaScript compiler

Andrés, on behalf of the standard library team
Ulf Norell | 29 Aug 10:24 2014

Agda 2.4.2

Agda 2.4.2 has been released.

Download with cabal install Agda-2.4.2 (might need cabal update first) or go to


- Recursive instance search.

  Instance arguments are much faster than before and now work
  like a proper class system.

- Major improvements to reflection

  - Quoting and unquoting of declarations and pattern matching lambdas.

  - New syntax to simplify using reflection:
      tactic f
    is sugar for
      quoteGoal g in unquote (f g)

/ Ulf
Agda mailing list
Jacques Carette | 28 Aug 03:02 2014

Termination problem with --without-K

[Probably related to (closed) issue 1214]

{-# OPTIONS --without-K #-}

open import Data.List
open import Data.Nat
open import Data.Bool

module Sort (A : Set) ( _≤_ : A → A → Bool) where
insert : A → List A → List A
insert x [] = []
insert x (y ∷ ys) with x ≤ y
... | true = x ∷ y ∷ ys
... | false = y ∷ insert x ys

This is reproducible in [And note that the above code is 
essentially verbatim from code on the Agda wiki]

Should I open a new bug?

Owen | 25 Aug 19:35 2014

Positivity of members of Set

Hello everyone,

It occurs to me that Chung-Kil Hur's proof can be viewed as an
infinite recursion arising from a negative occurrence of Set in a
constructor for Set. This is because the proof uses the excluded
middle only to "pattern match" on an element of Set -- that is, to
find out the type constructor for a type (where injectivity grabs the
type argument). In fact, the proof translates almost verbatim to an
ordinary datatype Set' where I : (Set' → Set') → Set'  is a
constructor, if the positivity check is disabled; then, the excluded
middle is not needed (and, again, injectivity grabs the constructor

Is there a compelling reason to allow Set to appear negatively within
Set? If a type constructor containing Set in a negative position were
required to be in Set₁, the issue would go away, and type constructors
could still be treated as injective.


> Hi everyone,
> I proved the absurdity in Agda assuming the excluded middle.
> Is it a well-known fact ?
> It seems that Agda's set theory is weird.
> This comes from the injectivity of inductive type constructors.
> The proof sketch is as follows.
> Define a family of inductive type
> data I : (Set -> Set) -> Set where
> with no constructors.
> By injectivity of type constructors, I can show that I : (Set -> Set) -> Set is injective.
> As you may see, there is a size problem with this injectivity.
> So, I just used the cantor's diagonalization to derive absurdity in a classical way.
> Does anyone know whether cantor's diagonalization essentially needs the classical axiom, or can be done
intuitionistically ?
> If the latter is true, then the Agda system is inconsistent.
> Please have a look at the Agda code below, and let me know if there's any mistakes.
> All comments are wellcome.
> Thanks,
> Chung-Kil Hur
> ============== Agda code ===============
> module cantor where
>   data Empty : Set where
>   data One : Set where
>     one : One
>   data coprod (A : Set1) (B : Set1) : Set1 where
>     inl : ∀ (a : A) -> coprod A B
>     inr : ∀ (b : B) -> coprod A B
>   postulate exmid : ∀ (A : Set1) -> coprod A (A -> Empty)
>   data Eq1 {A : Set1} (x : A) : A -> Set1 where
>     refleq1 : Eq1 x x
>   cast : ∀ { A B } -> Eq1 A B -> A -> B
>   cast refleq1 a = a
>   Eq1cong : ∀ {f g : Set -> Set} a -> Eq1 f g -> Eq1 (f a) (g a)
>   Eq1cong a refleq1 = refleq1
>   Eq1sym : ∀ {A : Set1} { x y : A } -> Eq1 x y -> Eq1 y x
>   Eq1sym refleq1 = refleq1
>   Eq1trans : ∀ {A : Set1} { x y z : A } -> Eq1 x y -> Eq1 y z -> Eq1 x z
>   Eq1trans refleq1 refleq1 = refleq1
>   data I : (Set -> Set) -> Set where
>   Iinj : ∀ { x y : Set -> Set } -> Eq1 (I x) (I y) -> Eq1 x y
>   Iinj refleq1 = refleq1
>   data invimageI (a : Set) : Set1 where
>     invelmtI : forall x -> (Eq1 (I x) a) -> invimageI a
>   J : Set -> (Set -> Set)
>   J a with exmid (invimageI a)
>   J a | inl (invelmtI x y) = x
>   J a | inr b = λ x → Empty
>   data invimageJ (x : Set -> Set) : Set1 where
>     invelmtJ : forall a -> (Eq1 (J a) x) -> invimageJ x
>   IJIeqI : ∀ x -> Eq1 (I (J (I x))) (I x)
>   IJIeqI x with exmid (invimageI (I x))
>   IJIeqI x | inl (invelmtI x' y) = y
>   IJIeqI x | inr b with b (invelmtI x refleq1)
>   IJIeqI x | inr b | ()
>   J_srj : ∀ (x : Set -> Set) -> invimageJ x
>   J_srj x = invelmtJ (I x) (Iinj (IJIeqI x))
>   cantor : Set -> Set
>   cantor a with exmid (Eq1 (J a a) Empty)
>   cantor a | inl a' = One
>   cantor a | inr b = Empty
>   OneNeqEmpty : Eq1 One Empty -> Empty
>   OneNeqEmpty p = cast p one
>   cantorone : ∀ a -> Eq1 (J a a) Empty -> Eq1 (cantor a) One
>   cantorone a p with exmid (Eq1 (J a a) Empty)
>   cantorone a p | inl a' = refleq1
>   cantorone a p | inr b with b p
>   cantorone a p | inr b | ()
>   cantorempty : ∀ a -> (Eq1 (J a a) Empty -> Empty) -> Eq1 (cantor a) Empty
>   cantorempty a p with exmid (Eq1 (J a a) Empty)
>   cantorempty a p | inl a' with p a'
>   cantorempty a p | inl a' | ()
>   cantorempty a p | inr b = refleq1
>   cantorcase : ∀ a -> Eq1 cantor (J a) -> Empty
>   cantorcase a pf with exmid (Eq1 (J a a) Empty)
>   cantorcase a pf | inl a' = OneNeqEmpty (Eq1trans (Eq1trans (Eq1sym (cantorone a a')) (Eq1cong a pf)) a')
>   cantorcase a pf | inr b = b (Eq1trans (Eq1sym (Eq1cong a pf)) (cantorempty a b))
>   absurd : Empty
>   absurd with (J_srj cantor)
>   absurd | invelmtJ a y = cantorcase a (Eq1sym y)
Mateusz Kowalczyk | 25 Aug 05:15 2014



I was running Agda over the categories library and watching htop and
noticed that Agda only uses a single core throughout: the whole run
looks like it does at [1].

I didn't see a --jobs or anything of the sort in --help. Is there any
real challenge of making Agda take advantage of multiple cores?
Considering it's written in Haskell it seems like it would be fairly
easy to do so. Of course it's hard to do so well but at least some
should be easy.


Mateusz K.
Sergei Meshveliani | 24 Aug 12:52 2014

explicit irrelevance

I am trying to replace the  irrelevance annotations  
with explicit irrelevance axioms ans proofs.
Consider the example:

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 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 =  case x ≟ 0# of \ { (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 =
                 case x ≟ 0#
                 of \
                 { (yes x=0) → ⊥-elim (x≉0 x=0)
                 ; (no x/=0) → 

Here  irrel-f  is used instead of the irrelevance annotation  
.(¬ x ≈ 0#)  in the signature for f.

And I need to prove  g=f-if.

≈refl  does not work. This is probably because there is no witness for
that  x≉0   and a value in  ¬ x ≈ 0#  used in the definition for  g  are
the same values.
For example, using  irrel-f  proves   f x x≉0 ≈ f x x/=0  
(in the context of `??'). 
But I do not see how to move it to  g.

Can anybody demonstrate a proof?


GRLMC - URV | 22 Aug 20:33 2014

LATA 2015: 2nd call for papers

*To be removed from our mailing list, please respond to this message with UNSUBSCRIBE in the subject line*



LATA 2015

Nice, France

March 2-6, 2015

Organized by:
CNRS, I3S, UMR 7271
Nice Sophia Antipolis University

Research Group on Mathematical Linguistics (GRLMC)
Rovira i Virgili University



LATA is a conference series on theoretical computer science and its applications. Following the
tradition of the diverse PhD training events in the field developed at Rovira i Virgili University in
Tarragona since 2002, LATA 2015 will reserve significant room for young scholars at the beginning of
their career. It will aim at attracting contributions from classical theory fields as well as
application areas.


LATA 2015 will take place in Nice, the second largest French city on the Mediterranean coast. The venue will
be the University Castle at Parc Valrose.


Topics of either theoretical or applied interest include, but are not limited to:

algebraic language theory
algorithms for semi-structured data mining
algorithms on automata and words
automata and logic
automata for system analysis and programme verification
automata networks
automata, concurrency and Petri nets
automatic structures
cellular automata
combinatorics on words
computational complexity
data and image compression
descriptional complexity
digital libraries and document engineering
foundations of finite state technology
foundations of XML
fuzzy and rough languages
grammars (Chomsky hierarchy, contextual, unification, categorial, etc.)
grammatical inference and algorithmic learning
graphs and graph transformation
language varieties and semigroups
language-based cryptography
parallel and regulated rewriting
power series
string and combinatorial issues in bioinformatics
string processing algorithms
symbolic dynamics
term rewriting
trees, tree languages and tree automata
unconventional models of computation
weighted automata


LATA 2015 will consist of:

invited talks
invited tutorials
peer-reviewed contributions


Paola Inverardi (L’Aquila), Synthesis of Protocol Adapters
Johann A. Makowsky (Technion, Haifa), Hankel Matrices for Graph Parameters and Graph Grammars
Giancarlo Mauri (Milano Bicocca), tba
Andreas Podelski (Freiburg), Automated Program Verification
Antonio Restivo (Palermo), The Shuffle Product: New Research Directions


Andrew Adamatzky (West of England, Bristol, UK)
Andris Ambainis (Latvia, Riga, LV)
Franz Baader (Dresden Tech, DE)
Rajesh Bhatt (Massachusetts, Amherst, US)
José-Manuel Colom (Zaragoza, ES)
Bruno Courcelle (Bordeaux, FR)
Erzsébet Csuhaj-Varjú (Eötvös Loránd, Budapest, HU)
Aldo de Luca (Naples Federico II, IT)
Susanna Donatelli (Turin, IT)
Paola Flocchini (Ottawa, CA)
Enrico Formenti (Nice, FR)
Tero Harju (Turku, FI)
Monika Heiner (Brandenburg Tech, Cottbus, DE)
Yiguang Hong (Chinese Academy, Beijing, CN)
Kazuo Iwama (Kyoto, JP)
Sanjay Jain (National Singapore, SG)
Maciej Koutny (Newcastle, UK)
Antonín Kučera (Masaryk, Brno, CZ)
Thierry Lecroq (Rouen, FR)
Salvador Lucas (Valencia Tech, ES)
Veli Mäkinen (Helsinki, FI)
Carlos Martín-Vide (Rovira i Virgili, Tarragona, ES, chair)
Filippo Mignosi (L’Aquila, IT)
Victor Mitrana (Madrid Tech, ES)
Ilan Newman (Haifa, IL)
Joachim Niehren (INRIA, Lille, FR)
Enno Ohlebusch (Ulm, DE)
Arlindo Oliveira (Lisbon, PT)
Joël Ouaknine (Oxford, UK)
Wojciech Penczek (Polish Academy, Warsaw, PL)
Dominique Perrin (ESIEE, Paris, FR)
Alberto Policriti (Udine, IT)
Sanguthevar Rajasekaran (Connecticut, Storrs, US)
Jörg Rothe (Düsseldorf, DE)
Frank Ruskey (Victoria, CA)
Helmut Seidl (Munich Tech, DE)
Ayumi Shinohara (Tohoku, Sendai, JP)
Bernhard Steffen (Dortmund, DE)
Frank Stephan (National Singapore, SG)
Paul Tarau (North Texas, Denton, US)
Andrzej Tarlecki (Warsaw, PL)
Jacobo Torán (Ulm, DE)
Frits Vaandrager (Nijmegen, NL)
Jaco van de Pol (Twente, Enschede, NL)
Pierre Wolper (Liège, BE)
Zhilin Wu (Chinese Academy, Beijing, CN)
Slawomir Zadrozny (Polish Academy, Warsaw, PL)
Hans Zantema (Eindhoven Tech, NL)


Sébastien Autran (Nice)
Adrian Horia Dediu (Tarragona)
Enrico Formenti (Nice, co-chair)
Sandrine Julia (Nice)
Carlos Martín-Vide (Tarragona, co-chair)
Christophe Papazian (Nice)
Julien Provillard (Nice)
Pierre-Alain Scribot (Nice)
Bianca Truthe (Giessen)
Florentina Lilica Voicu (Tarragona)


Authors are invited to submit non-anonymized papers in English presenting original and unpublished
research. Papers should not exceed 12 single-spaced pages (including eventual appendices,
references, etc.) and should be prepared according to the standard format for Springer Verlag's LNCS
series (see

Submissions have to be uploaded to:


A volume of proceedings published by Springer in the LNCS series will be available by the time of the conference.

A special issue of the Journal of Computer and System Sciences (Elsevier, 2013 JCR impact factor: 1.0) will
be later published containing peer-reviewed substantially extended versions of some of the papers
contributed to the conference. Submissions to it will be by invitation.


The period for registration is open from July 21, 2014 to March 2, 2015. The registration form can be found at:


Paper submission: October 10, 2014 (23:59 CET)
Notification of paper acceptance or rejection: November 18, 2014
Early registration: November 25, 2014
Final version of the paper for the LNCS proceedings: November 26, 2014
Late registration: February 16, 2015
Submission to the journal special issue: June 6, 2015




LATA 2015
Research Group on Mathematical Linguistics (GRLMC)
Rovira i Virgili University
Av. Catalunya, 35
43002 Tarragona, Spain

Phone: +34 977 559 543
Fax: +34 977 558 386


Nice Sophia Antipolis University
Rovira i Virgili University
Pepijn Kokke | 21 Aug 12:05 2014

Agda-mode and imported names

In agda-mode, when displaying values imported from modules with parameters, they are displayed as, e.g.


In addition, when using automatic rewriting, such as automatic casing (C-c C-c) the patterns are written as such.

Is there any way to avoid this, and have agda-mode use the simple imported name



Agda mailing list