Franck | 10 Sep 23:42 2014

ATVA 2014: Call for Participation

[We apologise for multiple copies.]


                 CALL FOR PARTICIPATION: ATVA 2014

       Automated Technology for Verification and Analysis

                      November 3--7, 2014

                       Sydney, Australia


         Early registration deadline: September 30, 2014



The purpose of ATVA is to promote research on theoretical and practical
aspects of automated analysis, verification and synthesis by providing
an international forum for interaction among the researchers in academia
and industry.


* Ahmed Bouajjani, LIAFA, Université Paris Diderot (Paris 7) Institut
Universitaire de France, France
(Continue reading)

Vladimir Voevodsky | 10 Sep 22:09 2014

postdoc position(s) announcement

The School of Mathematics at the Institute for Advanced Study in Princeton, NJ, 
is looking to fill one or more postdoc positions for the academic year 2015-16 
focusing on univalent formalization of mathematics in proof assistant Coq. 

The positions are for 1 year with a possible extension for an additional year. 

The areas of mathematics under consideration include classical homotopy theory of simplicial sets and
simplicial sheaves. 

The applicants should follow the standard application procedures outlined at:

In the "Field of work" in the application form please mention "Univalent Foundations".

Questions should be addressed to Vladimir Voevodsky at vladimir@...
Agda mailing list
James Chapman | 6 Sep 20:40 2014

AIM XX in Tallinn 16-22 October 2014

Dear all,

The next Agda meeting will be held in Tallinn, Estonia on 16-22 October 2014.

Preliminary information can be found here:

Further information will be forthcoming next week.

Mateusz Kowalczyk | 4 Sep 21:53 2014

Working with Agda inside nix-shell


I recently added an Agda builder to nixpkgs, the main repository for the
nix package manager and it works quite well.

nix has a feature called ‘nix-shell’ which lets you drop into the
project with all the dependencies available to you. As a result, I would
like to change what emacs calls out to when I press C-c C-l.

Here I have two problems.

I thought it would be as simple as

(setq agda2-program-name "nix-shell --pure --command agda") but it
wasn't, there is a separate args variable. But even if I eval:

(setq agda2-program-name "nix-shell")
(setq agda2-program-args '("--pure" "--command" "agda"))

It fails (details in a sec). I noticed in in agda-mode source that
‘--interaction’ is always cons'd in front of the argument list which
would make ‘nix-shell --interaction --pure --command agda’ but even if I
remove the cons and manually ensure it is passed in the right place, it

So at this point I'm stuck, unable to convince emacs to see the agda
inside my shell. It always fails with the following in *agda2* buffer:

Process Agda2 exited abnormally with code 1
IOTCM "/home/shana/programming/bitvector/Data/BitVector.agda"
(Continue reading)

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)