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
Sergei Meshveliani | 20 Aug 13:49 2014

irrelevant arg example

Dear Agda developers,

Agda of August 19 2014  type-checks irrelevant arguments in a different
way than  Agda-
So that some of my code is not type-checked any more.
I have the two questions on the subject.

1. Which treating is more correct?

2. For example, how to implement the function

  f : (x : ℕ) → .(nz : x ≢ 0) → x ≢ 0   
  f x ???



Hugo Herbelin | 18 Aug 17:58 2014

2nd CFP Post-proceedings TYPES 2014 Types for Proofs and Programs (open call)

2nd call for papers: Types for Proofs and Programs,
    post-proceedings of TYPES 2014 (open call)

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:   1 September 2014
Paper submission deadline:      8 September 2014
Notification of acceptance:    15 February  2015


* Papers must be submitted in PDF format using EasyChair:

* Authors have the option to include an attachment (.zip or .tgz)
  containing mechanised proofs, but reviewers are not obliged to take
  these attachments into account. Attachments will not be published.

* The post-proceedings will be published in LIPIcs (Leibniz
  International Proceedings in Informatics,
  ""), an open-access
  series of conference proceedings. Incidentally, publication of TYPES
  2013 post-proceedings is imminent as volume 26 of the LIPIcs series

* We recommend to keep the length of the contributions in the range of
  15-25 pages, and 25 pages is the upper limit for the submissions.


Hugo Herbelin           Inria Paris-Rocquencourt, France
Pierre Letouzey         University Paris-Diderot, France
Matthieu Sozeau         Inria Paris-Rocquencourt, France
Ekaterina Komendantskaya | 18 Aug 10:45 2014

Fully funded PhD position on Computational Logic/Functional Programming/Interactive Theorem Proving, University of Dundee, Scotland

One fully funded PhD position on Computational Logic/Functional Programming/Interactive Theorem Proving
is available at the University of Dundee, Scotland.

For more information, please email  katya <at> or refer to:

The funding is provided by EPSRC Doctoral Training Partnership Scheme, and is available for UK residents only.


Ekaterina Komendantskaya                 
Senior Lecturer, Head of PhD Studies                                      
Room 1.04, Queen Mother Building                                                       
School of Computing, University of Dundee                                                    
Scotland, DD14HN                                                                     
Tel: (+44) 01382384820                                                                                       

Agda mailing list
Roly Perera | 18 Aug 09:39 2014

Sized types problem


I'm modelling pi calculus in Agda and having difficulty using sized types in order to have the function ⊖ below pass the termination-checker. I'm also getting an error message which looks a bit odd, so perhaps there's a clue to what I'm doing wrong in there.

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

module Temp where

   open import Data.Product public hiding (swap)
   open import Relation.Binary.PropositionalEquality
   open import Size

   -- Processes.
   data Proc : Set where
      ν_ : Proc → Proc

   -- Actions.
   data ⟿ᵇ : Set where
      input : ⟿ᵇ
      boundOut : ⟿ᵇ

   data ⟿ᶜ : Set where
      out : ⟿ᶜ

   data ⟿ : Set where
      _ᵇ : ⟿ᵇ → ⟿
      _ᶜ : ⟿ᶜ → ⟿

   -- Renamings. Leave undefined for now.
   data Ren : Set where

      push : Ren
      swap : Ren
      _ᴬ*_ : Ren → ⟿ᶜ →  ⟿ᶜ

   -- Transitions.
   data _—[_]→_ : {ι : Size} → Proc → (a : ⟿) → Proc → Set where
      ν•_ : ∀ {ι P R} → _—[_]→_ {ι = ι} P (out ᶜ) R →
            _—[_]→_ {ι = ↑ ι} (ν P) (boundOut ᵇ) R
      νᵇ_ : ∀ {ι P R} {a : ⟿ᵇ} → _—[_]→_ {ι = ι} P (boundOut ᵇ) R →
            _—[_]→_ {ι = ↑ ι} (ν P) (a ᵇ) (ν R)
      νᶜ_ : ∀ {ι P R} → _—[_]→_ {ι = ι} P ((push ᴬ* out) ᶜ) R →
            _—[_]→_ {ι = ↑ ι} (ν P) (out ᶜ) (ν R)

   infixl 0 _—[_]→_

      _ᴾ*_ : Ren → Proc → Proc
      _ᵀ*_ : ∀ {ι} (ρ : Ren) {P R} {a : ⟿ᶜ} → _—[_]→_ {ι = ι} P (a ᶜ) R →
             _—[_]→_ {ι = ι} (ρ ᴾ* P) ((ρ ᴬ* a) ᶜ) (ρ ᴾ* R)
      swap-involutive : ∀ (P : Proc) → swap ᴾ* swap ᴾ* P ≡ P
      swap∘push : swap ᴬ* push ᴬ* out ≡ out

   infixr 8 _ᵀ*_ _ᴾ*_ _ᴬ*_

   -- Structural congruence.
   infix 4 _≅_
   data _≅_ : Proc → Proc → Set where
      νν-swap : ∀ P → ν (ν (swap ᴾ* P)) ≅ ν (ν P)

   -- "Residual" of a transition E after a structural congruence φ.
   ⊖ : ∀ {ι P P′} {a : ⟿} {R} (E : _—[_]→_ {ι = ι} P a R) (φ : P ≅ P′) →
       Σ[ R ∈ Proc ] _—[_]→_ {ι = ι} P′ a R
   ⊖ (ν•_ (νᶜ E)) (νν-swap P) with swap ᵀ* E
   ... | swap*E rewrite swap-involutive P | swap∘push =
      _ , {!!} -- νᵇ (ν• swap*E)
   ⊖ E φ = {!!}

(I can try to boil the code down further if that would help, but I wanted to maintain some of the structure of my setting.)

In the first goal above, I'm matching on the situation where there are adjacent ν binders, and showing that if I transpose the binders (by applying the 'swap' renaming under the binders) then the associated steps in the derivation also tranpose. Intuitively this preserves the size of the transition derivation. And indeed, toggling hidden arguments reveals that the goal has type _—[_]→_ {↑ (↑ .ι)}, so I expect to be able to apply two constructors (νᵇ and ν• in this case) in return for two I eliminated (ν• and νᶜ). 

I can also see that E has type _—[_]→_ {.ι}. Since I've postulated that ᵀ* is size-preserving, the variable swap*E also has this type. Naively, I expect νᵇ (ν• swap*E) to therefore be size-consistent with the goal. However Agda complains that the constraints are inconsistent.

Weirdly, if I use a "with" clause to introduce ν• swap*E into the context, I get the following error:

.ι !=< P of type Size
when checking that the expression E has type
swap ᴾ* P —[ (push ᴬ* out) ᶜ ]→ .R

This is baffling because the appearance of meta-variable P in the error message suggests that Agda is trying to match a size index against a variable of type Proc, does it not?

Can anyone shed any light on what's going on here?

many thanks,

Roly Perera
LFCS, School of Informatics
University of Edinburgh

Agda mailing list
planpublicity | 14 Aug 21:53 2014

Second call for papers IFL 2014


Please, find below the second call for papers for IFL 2014.
The submission page is now open.

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





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.


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 2014 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

Following the IFL tradition, IFL 2014 will use a post-symposium review
process to produce the formal proceedings. All participants of IFL
2014 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 do not count as
publication for 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.

Submission Details

Submission deadline draft papers:                          September 1 
Notification of acceptance for presentation:               September 5
Early registration deadline:                               September 10
Late registration deadline:                                September 17 
Submission deadline for pre-symposium proceedings:         September 24
26th IFL Symposium:                                        October 1-3 
Submission deadline for post-symposium proceedings:        December 15
Notification of acceptance for post-symposium proceedings: January  31 2015
Camera-ready version for post-symposium proceedings:       March    15 2015 

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 adhere to the standard ACM two columns conference format. 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. A suitable document template for LaTeX can be found at:

Papers should be submitted online at


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 2014, please contact the PC chair at
samth@... Topics of interest include, but are not limited

•  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 honoured 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

Sam Tobin-Hochstadt, Indiana University (Chair)
Rinus Plasmeijer, Radboud University Nijmegen (Co-Chair)
Atze Dijkstra, Utrecht University
Colin Runciman, University of York
Graham Hutton, University of Nottingham
Mary Sheeran, Chalmers University of Technology
Patricia Johann, Appalachian State University
Matthew Fluet, Rochester Institute of Technology
Josef Svenningsson, Chalmers University of Technology
Małgorzata Biernacka, University of Wroclaw
Peter Achten, Radboud Univerity Nijmegen
Laura Castro, University of A Coruña
Hai Paul Liu, Intel Labs
Kathryn Gray, Cambridge University
Lars Bergstrom, Mozilla Research
Lindsey Kuper, Indiana University
Nicolas Wu, Oxford
T. Stephen Strickland, University of Maryland
Xavier Clerc, INRIA


The 26th IFL will be held in association with the College of Computer
and Information Science at Northeastern University. It can be reached
quickly and easily by public transport.
Sergei Meshveliani | 13 Aug 20:16 2014

all-P ?


I program  

  open import Data.List.All as All using () 
                                   renaming ([] to []a; _∷_ to _∷a_)
  all-P : {A : Set} {P : A → Set} (p : (x : A) → P x) → (xs : List A) →
                                                            All.All P xs
  all-P p []       = []a
  all-P p (x ∷ xs) = p x ∷a (all-P p xs)

and use it like in this example:

  record Item : Set where field val   : ℕ
                                val>0 : val > 0
  open Item

  foo : (its : List Item) → All.All (\i → val i > 0) its
  foo = all-P val>0

The idea is to apply  all-P  instead of a recursive implementation for
each new function instead of  val>0.

Am I missing something?
Can this be achieved in a simpler way than by  all-P ?
I thought of,  but it occurs that it does not fit.  
Has Standard library something like  all-P ?



Sergei Meshveliani | 12 Aug 14:36 2014

hiding implementation


there is the following effect in Agda (of July 2014).
There are some programs of kind 

  foo : <signature>
  foo x =  <implementation>

  -- in another module ----
  f : <signature2>
  f y =  ...
         foo y       -- using  foo

They are type-checked.
And if we                      postulate foo : <signature>
and remove its implementation,
then Agda reports an error for  f  for the place where  foo  is applied.

Such cases as with  foo and f  are rare, but they present in my

Is this an error in Agda ?


Sergei Meshveliani | 11 Aug 18:50 2014

about Null


I introduce 

  data Null {α} {A : Set α} : List A → Set α  where  isNull : Null []

for expressing the predicate  "a list is empty". 
Then, I need to prove the following two simple statements
(¬Null→length>0, a ≢ 0). And fail.
Can you, please demonstrate a proof?

open import Level using (Level)
open import Function using (case_of_)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Data.Empty       using (⊥; ⊥-elim)
open import Data.Nat         using (ℕ; suc; _>_; _≤_; s≤s; z≤n)
open import Data.List        using (List; []; _∷_; length)
open import Data.Product     using (_,_)

data Null {α} {A : Set α} : List A → Set α  where  isNull : Null []

null? : {α : Level} → {A : Set α} → (xs : List A) → Dec (Null xs)
null? []      = yes isNull
null? (_ ∷ _) = no λ()

suc>0 : ∀ {n} → suc n > 0
suc>0 = s≤s z≤n

¬Null→length>0 : {α : Level} → {A : Set α} → (xs : List A) → ¬ Null xs →
                                                           length xs > 0
¬Null→length>0 (_ ∷ _) _  =  suc>0
¬Null→length>0 [] ()                 -- fails

-- Prove  a ≢ 0  from these postulated things:

postulate anything      : ∀ {a} {A : Set a} → A
          items         : ℕ → List ℕ
          a             : ℕ
          nullItems→a≢0 : Null (items a) → a ≢ 0
          lnItems>0→a≢0 : length (items a) > 0 → a ≢ 0

a≢0 : a ≢ 0
a≢0 = go (items a) PE.refl (null? (items a))
    go : (its : List ℕ) → its ≡ (items a) → Dec (Null (items a)) → a ≢ 0
    go _ _ (yes nullIts-a)   =  nullItems→a≢0 nullIts-a
    -- go _ _ (no notNullIts-a =  
    -- ?
Sergei Meshveliani | 10 Aug 19:58 2014

"data Null" for List


a function  foo  needs an argument stating that a certain list is empty:

  foo : (null primaryItems ≡ true) → Foo 

And this expression with  "≡ true"  looks awkward.

Has it sense to introduce

  data Null {α} {A : Set α} : List A → Set α  where  isNull : Null []  

and then, to write

  foo : Null primaryItems → Foo 
  foo isNull = ...


Sergei Meshveliani | 10 Aug 16:16 2014

with vs case example


how to change the below `with' to `case' ? 

 foo : a ∣ 1# → (null pItems ≡ true)
 foo a∣1
         with pItems
 ... | []       =  PE.refl
 ... | item ∷ _ =  ⊥-elim $ a∤1 a∣1
                   postulate a∤1 : a ∤ 1#

 {- variant 
 foo a∣1 =  case pItems of \ { []         → PE.refl 
                             ; (item ∷ _) → let a∤1 : a ∤ 1#
                                                a∤1 = anything 
                                            in  ⊥-elim $ a∤1 a∣1     

`with' is type-checked, and `case' is not.