Sergei Meshveliani | 27 Nov 14:05 2014

termination for nested construct

I have a recursion of kind 

 f : Foo → Set    
 f (foo (foo' (x ∷ xs) prop'-x:xs) prop-x:xs) = ... 
                              d = f (foo (foo' xs prop'-xs) prop-xs)

where  foo  and  foo'  are the two record constructors, and recursion is
by changing  x :: xs  -->  xs.

Agda- does not see termination here.

What is the simplest method to prove termination for f ?

I apply the following approach. Extract  xs  from the Foo data and use
it as an additional argument in 'prove'. But this needs also to equate
this argument in `prove' to the list in the Foo data. So that the
function becomes

 f (foo (foo' xs prop') prop) =                   
                        prove (foo (foo' xs prop') prop) xs PE.refl    
   prove : (d : Foo) → (xs : List C) → list d ≡ xs → Set 

   prove _ [] _ =  =foo-refl      
   prove (foo (foo' (x ∷ xs) prop'x:xs) prop-x:xs) 
                                        (.x ∷ .xs) PE.refl =  ...
(Continue reading)

Thorsten Altenkirch | 27 Nov 11:03 2014

Maxime Dene's bug fixed

Not long ago Maxime Denes reported a problem with Coq which lead to it being incompatible with univalence. Also it meant that there are programs definable by structural recursion which are not derivable using eliminators. This was also applicable to Agda even with the without-K flag turned on. One version of the bug in Agda (by Conor) is below.

My question is: is this bug fixed in the current versions of Agda and Coq?

Next question: how can we make sure that there are no other issues of this kind?


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

module BadWithoutK where

data Zero : Set where

data WOne : Set where
  wrap : (Zero -> WOne) -> WOne

data _<->_ (X : Set) : Set -> Set where
  Refl : X <-> X

  myIso : WOne <-> (Zero -> WOne)

moo : WOne -> Zero
noo : (X : Set) -> (WOne <-> X) -> X -> Zero

moo (wrap f) = noo (Zero -> WOne) myIso f
noo .WOne Refl x = moo x

bad : Zero
bad = moo (wrap \ ())

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

Agda mailing list
edprocess | 27 Nov 06:45 2014

INTECH 2015 <at> Spain

Fifth International Conference on Innovative Computing Technology  
(INTECH 2015)
University of Vigo, Galicia, Spain
May 20-22, 2015
Technically co-sponsored by IEEE UK & RI
Proceedings will be published in IEEE xplore

The First international conference on Innovative Computing Technology  
(INTECH 2011) was held at Sao Carlos in Brazil followed by the Second  
International Conference on Innovative Computing Technology (INTECH  
2012) at Casablanca in Morocco. The INTECH 2013 and INTECH 2014 were  
organized at London and Luton, UK respectively. The INTECH 2015 is  
organized by the Atlantic Research Centre for Information and  
Communication Technologies of the University of Vigo, Spain.  The  
INTECH 2015 offers the opportunity for institutes, research centers,  
engineers, scientists and industrial companies to share their latest  
investigations, researches, developments and ideas in area of  
Innovative Computing Technology, which covers huge topics.

The INTECH intends to address various innovative computing techniques  
involving various applications. This forum will address a large number  
of themes and issues. The conference will feature original research  
and industrial papers on the theory, design and implementation of  
computing technologies, as well as demonstrations, tutorials,  
workshops and industrial presentations. This conference (INTECH 2015)  
will include presentations of contributed papers by invited keynote  

Conference papers will include innovative computing paradigms in the  
following topics:

    Network and Information Security				   Algorithms
    Innovative Computing Systems and Applications in S & T domains 	    
Applied Information Systems
    Artificial Intelligence and Decision Support Systems		    
Broadcasting Technology
    Data and Network mining					   Cloud Computing
    Computational Intelligence					   Green Computing
    Data Stream Processing in Mobile/Sensor Networks		   Grid computing
    Database Systems						   Internet of Things
    Digital Image/Video Processing					   Mobile network and systems
    E-Learning, e-Commerce, e-Business and e-Government		    
Human-Computer Interaction
    Intelligent Condition Monitoring					   Multimedia and Interactive  
    Peer-to-peer social networks					   Signal Processing
    Software Engineering						   Ubiquitous Computing
    User Interfaces, Visualization and Modeling			   Virtual Reality
    WWW Applications and Technologies				   Visualization
    XML and other Extensible Languages				   Web services
    Soft Computing: Fuzzy and Neural Network Systems, optimization algorithms

The INTECH proceedings will also be indexed by dblp. All the papers  
will be reviewed and the accepted papers in the conference will be  
submitted to IEEE Xplore for indexing and will be indexed in many  
global databases.In addition, all the accepted papers (for Journals)  
will be published in the following special issues journals after  
substantial revision and modification.

Journal of Digital Information Management (JDIM) (Scopus and EI Indexed)
International Journal of Enterprise Information Systems (Scopus and EI  
International Journal of Grid and High Performance Computing (IJGHPC)  
(Scopus and EI Indexed)
International Journal of Computational Science and Engineering   
(Scopus and EI Indexed)
International Journal of Big Data Intelligence
International Journal of Applied Decision Sciences (Scopus/EI)
International Journal of Management and Decision Making (Scopus/EI)
International Journal of Enterprise Information Systems (Scopus/EI)


General Chairs
José Juan Pazos-Arias, Universida de Vigo, Spain
Martín López-Nores, Universida de Vigo, Spain
Ezendu Ariwa, University of Bedfordshire, UK

Program Chairs
Manuel Ramos-Cabrer, Universida de Vigo, Spain
Aziz El Janati El Idrissi, Mohammed V Agdal University, Morocco

Publicity Chair
Alberto Gil-Solla , Universida de Vigo, Spain

Organization Chair
Yolanda Blanco-Fernández , Universida de Vigo, Spain


Submission of papers: March 01, 2015
Notification of Acceptance/Rejection: April 01, 2015
Camera Ready:May 01, 2015
Registration:May 01, 2015
Conference:May 20-22, 2015

Submission URL:
Email: intech@...
Andrés Sicard-Ramírez | 26 Nov 16:07 2014



Agda has been released.

This is a bug-fix release fixing compilation on Windows and others issues.

The standard library 0.9 type-checks with this version of Agda.

Download with

  cabal update && cabal install Agda

or got to .
Andrés, on behalf of the Agda team
Agda mailing list
Guillaume Brunerie | 26 Nov 14:33 2014

Telescope syntax

Hello all,

As is well known, it’s currently a bit annoying to use universe
polymorphism in Agda because instead of writing

  f : (A B C : Type) -> …

you have to write

  f : {i j k : Level} (A : Set i) (B : Set j) (C : Set k) -> …

Would it be a good idea to make the first one a syntactic sugar for
the second one?
I’m thinking about adding a "telsyntax" keyword, such that you can
write for instance

  telsyntax {i : Level} (X : Set i) = (X : Type)

and then (A B C : Type) (in a telescope) would be automatically translated into

  {i : Level} (A : Set i) {j : Level} (B : Set j) {k : Level} (C : Set k)

And this is not just about universe management, but it would also be
very useful when using instance arguments. For instance if a group is
a type (of level 0, say) with a group structure (which will be found
by instance search), and you want to write a function taking three
groups as arguments you have to write

  g : (G H K : Set) {{_ : GroupStr G}} {{_ : GroupStr H}} {{_ :
GroupStr K}} -> …

But you could say instead

  telsyntax (G : Set) {{_ : GroupStr G}} = (G : Group0)
  g : (G H K : Group0) -> …

And of course you can combine the two, if groups can be at any
universe level then the following:

  telsyntax {i : Level} (G : Set i) {{_ : GroupStr G}} = (G : Group)
  g : (G H K : Group) -> …

would be a shorthand for

  g : {i j k : Level} {G : Set i} {H : Set j} {K : Set k} {{_ :
GroupStr G}} {{_ : GroupStr H}} {{_ : GroupStr K}} -> …

which is much less readable and annoying to write.

One drawback (in the case of universe levels) is that you don’t have
access to the level anymore, but I don’t think that would really be a
problem, and you still can make the levels explicit if you need to.
Another drawback is that when writing (A : Type) or (G : Group) in a
telescope, it makes it look like Type and Group are types, but it’s
not the case so it could be confusing (for instance you can’t end a
function with "-> Group"). If that’s indeed too confusing, maybe we
could use a different notation than a colon, to make it clear that
it’s just syntactic sugar (on the other hand, it looks nice with a

What do you think?

Christopher Jenkins | 23 Nov 23:39 2014

Possible bug when using "with" on a partially applied function

I am aware that a function generated by "with" is not always well-typed. I'm to understand this is limited to cases where, for example, function foo takes as its argument B (bar a), where a : A and B : A -> Set, and we have rewritten "bar a" to some "w", but foo remains untouched (i.e. its external to the context).

However, this is not that situation here. Agda has mysteriously eaten n : Nat, and replaced its occurrences with a : A (a parametric type), generating a type error. I can't imagine this is anything other than a bug, but if it isn't I'd at least like to know the rationale behind this behaviour.

Note that I am aware that this definition of "swap" is terrible. I was playing with Agda to see if I could push it to see the function is involutive even in such a situation when I encountered this.


Christopher Jenkins
Computer Science 2013
Trinity University
Agda mailing list
Sergei Meshveliani | 20 Nov 11:55 2014

strange PE.refl ambiguity

I have

  open import Relation.Binary.PropositionalEquality as PE using (_≡_)

  addMany : List C×ℕ → Multiset → Multiset
  addMany ps mS =  foldr add1 mS ps


  cong₂addMany : {ps : List C×ℕ} → (addMany ps) Preserves _=ms_ ⟶ _=ms_

  cong₂addMany {[]}     {_}  {_}   mS=ms=mS' =  mS=ms=mS'
  cong₂addMany {p ∷ ps} {mS} {mS'} mS=ms=mS' =
      addMany (p ∷ ps) mS      =ms[ =ms-reflexive (lemma mS) ]

                            -- =ms[ =ms-reflexive PE.refl]

      add1 p (addMany ps mS)   =ms[ cong₂add1 {p} $ cong₂addMany {ps}
                                                    {mS} {mS'} mS=ms=mS'
      add1 p (addMany ps mS')  =ms[ =ms-reflexive $ lemma mS' ]
      addMany (p ∷ ps) mS'
    lemma : (s : Multiset) → addMany (p ∷ ps) s ≡ add1 p (addMany ps s)
    lemma _ = PE.refl

Here 'lemma'  is only by normalization by the definition of

And I do not understand:  why replacing  (lemma mS)  with  PE.refl
leads to "unsolved metas".
How to avoid writing additional signatures after `where' which actually
express only  PE.refl ?
In earlier examples, it worked merely PE.refl instead of a similar
lemma. And this particular example occurs "unsolved", and adding `lemma'
complicates the code.


CIE | 20 Nov 08:53 2014

Final Call - 12th Annual Conference on Theory and Applications of Models of Computation (TAMC 2015), Singapore 18-20 May, 2015

Final Call for Papers for the 12th Annual Conference on

  Theory and Applications of Models of Computation (TAMC 2015)
  18 - 20 May 2015 (Submission Deadline 27 November 2014)
  Deadline 27 November 2014

School of Computing, National University of Singapore

TAMC 2015 aims at bringing together a wide range of researchers with
interests in computational theory and applications. For more than 10
years, the conference series "Theory and Applications of Models of
Computing" has fostered interactions and collaborations between both
theoretical and applied researchers working on all aspects of
computations and the ways to model it.

Invited Speakers:
Lance Fortnow (Georgia Institute of Technology),
Miklos Santha (CNRS, Univ. Paris Diderot and CQT, Nat. Univ. of Singapore),
Alexandra Shlapentokh (East Carolina University).

Conference Chair: Sanjay Jain.
Programme Committee Chairs: Rahul Jain and Frank Stephan.
Programme Committee: Ajith Abraham, Anthony Bonato, Yijia Chen, Rodney
G. Downey, Henning Fernau, Dimitris Fotakis, Gopal T V, Steffen Lempp,
Jiamou Liu, Frederic Magniez, Klaus Meer, Mia Minnes, Philippe
Moser, Mitsunori Ogihara, Yota Otachi, Yicheng Pan, Pan Peng, Anil
Seth, Xiaoming Sun, Chaitanya Swamy, Hongan Wang, Wei Wang, Guohua Wu,
Yitong Yin, Mingsheng Ying, Neal Young, Thomas Zeugmann, Shengyu
Zhang, Conghua Zhou.

Submission due: Thu 27 November 2014 at 23:59 hrs GMT.
Notification: Tue 20 January 2015.
Final Version due: Tue 3 February 2015.
Conference: Mon 18 - Wed 20 May 2015

Proceedings: The proceedings of TAMC 2015 will appear in the
Springer LNCS series. Submissions should be 12 pages in llncs-format.
For details on submissions and other aspects, please consult the
TAMC 2015 homepage at

Topics: TAMC 2015 is open for all topics relating to the theory and
applications of models of computation. The topics include algebraic
computation, algorithmic coding and number theory, algorithmic
learning theory, approximation algorithms, automata theory, circuit
complexity, communication complexity, complex networks and their
theory, combinatorial algorithms, computability and recursion theory,
computational biology, computational complexity, computational
geometry, continuous and real computation, cryptography, data
structures, design and analysis of algorithms, distributed algorithms,
domain models, fixed parameter tractability, formal languages, game
theory, geometric algorithms, grammatical inference, graph algorithms,
graph mining, information theory, internet mathematics, memory
hierarchy tradeoffs, model theory for computing, natural computing,
network algorithms, network security and applications, online
algorithms, optimisation, parallel algorithms, philosophy of
computing, privacy and security, property testing, proof complexity,
process models, quantum computation, randomness, randomised
algorithms, space-time tradeoffs, streaming algorithms, systems
theory, VLSI models of computation.

TAMC in previous years: The conference series TAMC started in the year
2004 and has been held annually since then. The previous conferences
are the following: Beijing China 2004, Kunming China 2005, Beijing
China 2006, Shanghai China 2007, Xian China 2008, Changsha China 2009,
Prague Czech Republic 2010, Tokyo Japan 2011, Beijing China 2012, Hong
Kong China 2013, Chennai India 2014. 
Aaron Stump | 19 Nov 21:31 2014
Picon installation issue

Hi, Agda community.

I am trying to help a student get Agda installed on his Ubuntu 
14.04 computer, and we are getting this error message (we are using 
local version of cpphs, happy, and alex, because the ones we get with 
apt-get seem to be too old):

paco <at> lucio:~$ cabal --with-cpphs="/home/paco/.cabal/bin/cpphs" 
--with-alex="/home/paco/.cabal/bin/alex" install Agda
Resolving dependencies...
[1 of 1] Compiling Main             ( 
/tmp/Agda- )
Linking /tmp/Agda- ...
Configuring Agda-
Building Agda-
Preprocessing library Agda-

     Could not find module `System.Time'
     It is a member of the hidden package `old-time-'.
     Perhaps you need to add `old-time' to the build-depends in your 
.cabal file.
     Use -v to see a list of the files searched for.
Failed to install Agda-
cabal: Error: some packages failed to install:
Agda- failed during the building phase. The exception was:
ExitFailure 1

Any ideas what is happening here?  I assume this must be some issue with 
the configuration of Haskell, not Agda (I have compiled Agda on 
my own computer with the same version of ghc (7.6.3) as the student's, 
with no problems).

Andrés Sicard-Ramírez | 15 Nov 01:23 2014

ANNOUNCE: Standard library 0.9


The standard library 0.9 has been released (see

The library has been tested using Agda

Important changes since 0.8.1:

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
Agda mailing list
Andrés Sicard-Ramírez | 15 Nov 01:21 2014



Agda has been released.

Download with

  cabal update && cabal install Agda

Important changes since Agda 2.4.2:

Andrés, on behalf of the Agda team
Agda mailing list