gmane.comp.lang.agda

SSTiC 2013: next registration deadline 26 May

GRLMC — 2013-05-19T13:36:37

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

*********************************************************************

2013 INTERNATIONAL SUMMER SCHOOL ON TRENDS IN COMPUTING

SSTiC 2013

Tarragona, Spain

July 22-26, 2013

Organized by
Rovira i Virgili University

http://grammars.grlmc.com/SSTiC2013/

*********************************************************************

+++ next registration deadline: May 26 +++

*********************************************************************

AIM:

SSTiC 2013 will be an open forum for the convergence of top class well
recognized computer scientists and people at the beginning of their research
career (typically PhD students) as well as consolidated researchers.

SSTiC 2013 will cover the whole spectrum of computer science by means of 63
six-hour courses dealing with hot topics at the frontiers of the field. By
actively participating, lecturers and attendees will share the idea of
scientific excellence as th

LCC'13 : Workshop on Logic and Computational Complexity

Arnaud Durand — 2013-05-17T16:38:44

[ Please broadcast/post/forward.   Apologies for duplicates]

LCC'13 WORKSHOP ANNOUNCEMENT

The Fourteenth International Workshop on Logic and Computational Complexity
(LCC'11,http://www.cs.swansea.ac.uk/lcc2013/)
will be held in Torino on September 6, 2013, as an affiliated meeting
of CSL'13 (http://csl13.di.unito.it/).

LCC meetings are aimed at the foundational interconnections between 
logic and computational complexity, as present, for example,  in 
implicit computational complexity (descriptive and type-theoretic 
methods); deductive formalisms as they relate to complexity (e.g. 
ramification, weak comprehension, bounded arithmetic, linear logic and 
resource logics); complexity aspects of finite model theory and 
databases; complexity-mindful program derivation and verification; 
computational complexity at higher type; and proof complexity.

The LCC'13 program will consist of invited lectures as well as selected 
contributed papers. We welcome informal presentations about work in 
progress, survey pa

Re: isHead x (x :: xs)

Paolo Capriotti — 2013-05-17T09:07:54

isHP : (x : ℕ) → (xs : List ℕ) → isHead x (x ∷ xs) ≡ true
isHP x xs with x ≟ x
... | yes _ = refl
... | no p = ⊥-elim (p refl)

As a general rule of thumb, a proof about a function defined by cases
usually needs to have the same cases, so that beta-reduction can
happen in each of them.

Paolo

isHead x (x :: xs)

Sergei Meshveliani — 2013-05-17T08:57:09

Please, how to prove the following?

  isHead : ℕ → List ℕ → Bool
  isHead _ []        = false 
  isHead x (y ∷ ys)  with  x ≟ y
  ...              | yes _ = true 
  ...              | no _  = false 

  isHP : (x : ℕ) → (xs : List ℕ) → isHead x (x ∷ xs) ≡ true
  isHP x xs =
              ??

Thanks,

------
Sergei

CiE 2013 in Milan, July 1 - 5: First Call for Participation

S B Cooper — 2013-05-16T12:06:33

---------------------------------------------------------------------------
       COMPUTABILITY IN EUROPE 2013: The Nature of Computation
                       Milan, Italy,  July  1 - 5, 2013

                           CALL FOR PARTICIPATION

                 Informal Presentation Deadline: 31 May 2013
                   Early Registration Deadline: 31 May 2013

                      http://cie2013.disco.unimib.it

                 co-located with
         Unconventional Computation and Natural Computation 2013

             http://ucnc2013.disco.unimib.it
---------------------------------------------------------------------------

TUTORIAL SPEAKERS:  Gilles Brassard (Universite de Montreal) and
Grzegorz Rozenberg (Leiden Institute of Advanced Computer Science and 
University of Colorado at Boulder)

PLENARY TALKS:
Ulle Endriss (University of Amsterdam)
Lance Fortnow (Georgia Institute of Technology)
Anna Karlin (University of Washington)
Bernard Moret (Ecole Polytechnique Federale de Lausanne)
Mariya So

Final CFP: INTECH 2013 at BCS

edprocess — 2013-05-17T05:20:04

Call for Papers 


The Third International Conference on Innovative Computing Technology 
(INTECH 2013)
August 29-31, 2013
British Computer Society, London, UK
Technically co-sponsored by IEEE UK & RI
Proceedings will be indexed in IEEE Xplore
(Http://www.dirf.org/intech) 


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 third conference will be held at British Computer 
Society during August 29-31, 2013. The INTECH 2013 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 
t

Re: Implementation of abstract vs. irrelevance

Andrea Vezzosi — 2013-05-16T20:13:37

It seems I was completely wrong when blaming instantiation, the vast
majority of the time is spent pretty-printing function calls to populate
the CallInfo in Calls, maybe there's a way to store the call itself and the
needed context in Calls and only pretty-print if there's a need, for error
messages I guess, later?

I've also implemented a simple traversal that checks if there's circularity
in a mutual block and skips termination checking if there isn't, it seems
to get back almost the original speedup for Adjunction.agda, if
typechecking the std-lib doesn't get slower I will prepare a patch.

Cheers,
  Andrea


On Mon, May 13, 2013 at 9:53 PM, Andrea Vezzosi <sanzhiyan-Re5JQEeQqe8AvxtiuMwx3w< at >public.gmane.org> wrote:

_______________________________________________
Agda mailing list
Agda-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB< at >public.gmane.org
https://lists.chalmers.se/mailman/listinfo/agda

DTP 2013 2nd Call For Papers

Stephanie Weirich — 2013-05-16T17:38:44

========================================================================

                               DTP 2013

           ACM SIGPLAN Workshop on Dependently-Typed Programming

                             24th SEPTEMBER 2013
                          Boston, Massachusetts, USA                    
                       (co-located with ICFP 2013)

                          2nd CALL FOR PAPERS

             http://www.seas.upenn.edu/~sweirich/dtp13
========================================================================

[NOTE: Compared to the first announcement, this CFP updates the workshop 
date, submission deadline, and also solicits informal presentations for DTP.]

Overview
--------

The ACM SIGPLAN Workshop on Dependently-Typed Programming 2013 will be
co-located with the [2013 International Conference on Functional Programming
(ICFP), in Boston, Massachusetts, USA](http://icfpconference.org/icfp2013/).

The purpose of DTP is to discuss experiences with dependent types in
programming and future de

Re: Defining a module by pattern matching

Andreas Abel — 2013-05-16T08:22:43

What works is

module ModuleArguments {x y : A} (p : x ≡ y) (u : B x) (v : B y) where
   thing' : tr p u ≡ v → u ≡ tr! p v
   thing' h with y | p  | v
   thing' h | .x | refl | v = h

Since matching on p refines y to x, you need to with-abstract also over 
y and v, which mentions y in its type.

What exactly would be your proposal?  That module parameters can be 
refined by unification during pattern matching (as Nisse proposed)?

Cheers,
Andreas

On 15.05.13 10:37 PM, Guillaume Brunerie wrote:

Re: Defining a module by pattern matching

Guillaume Brunerie — 2013-05-15T20:37:18

Hmm, interesting. It wasn’t an EQUALITY built-in, but now it is and
your example works.
It’s getting closer, but it’s still not exactly what I want. Here is a
more concrete example (I don’t have the standard library, so maybe it
doesn’t compile as is)


module Guillaume {A : Set} {B : A → Set} where

open import Relation.Binary.PropositionalEquality

Re: Defining a module by pattern matching

Nils Anders Danielsson — 2013-05-15T20:14:18

I noted this problem in a feature request back in 2007, before we
started using the bug tracker:

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.ModuleSystemMoreFlexible

Re: Defining a module by pattern matching

Dr. ERDI Gergo — 2013-05-15T20:06:13


Is your equality type a valid EQUALITY built-in? Because I was able to get 
this working via 'rewrite', which requires _≡_ (or in your case, _==_) to 
be marked as the EQUALITY:

module Guillaume where

open import Relation.Binary.PropositionalEquality

module FunctionArguments where
   same-same : {A : Set} {x y : A} {P : A → Set} → x ≡ y → P x → P y
   same-same refl Px = Px

module ModuleArguments {A : Set} {x y : A} {eq : x ≡ y} where
   same-same : {P : A → Set} → P x → P y
   same-same Px rewrite eq = Px

Re: Defining a module by pattern matching

Guillaume Brunerie — 2013-05-15T19:45:59

Hi Gergo,

This looks like a good idea but I don’t see how to make it work with
pattern matching on the identity type instead.
The issue is that the identity type is an inductive family, so when
pattern matching against it it will change one of the endpoints (which
is another module argument) so Agda does not like it.

Guillaume

2013/5/15 Dr. ERDI Gergo <gergo-RKenwXofdno< at >public.gmane.org>:

Re: Defining a module by pattern matching

Dr. ERDI Gergo — 2013-05-15T19:18:33


Would something like ths help?

module Guillaume where

open import Data.Bool

Defining a module by pattern matching

Guillaume Brunerie — 2013-05-15T19:05:49

Hi,

I have several definitions all starting with the following arguments:
{x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}

In order to make the code more readable, I would like to wrap them in
a section so that I can write the arguments only once.
The issue is that all those definitions are defined by pattern
matching on p, so I cannot do it and I need to copy paste the list of
arguments for each definition which makes the code quite hard to read.

Is there a way to workaround this issue? Some way to define a
parametrized module by pattern matching, or something like that?

Thanks,

Guillaume

Re: `abstract' on Web keywords

Serge D. Mechveliani — 2013-05-15T12:23:27

I am trying to understand your consideration.
Probably, you talk of introducing some  careless-abstract  to the 
Language.
careless-abstract  will be possible to set in such places where I 
tried to set `abstract' and failed 
(by "freesing signature", and hence, by "unsolved metas" ?).

Do I understand correct?


1. In this particular case I aimed at the    type-check performance,
   namely -- at reducing its memory eagerness.

2. I do not uderstand how can one win in the  type-check performance
   by abstracting something and in the same time not hiding 
   implementation details.
When a function body of  f  is  not unfold  in the outer place where 
it is called, then I think, the implementation details of  f  
"are hidden" (?). 
If it is unfold there, then the type-check is space-eager, and 
performance is down.

Is `abstract' similar to  inline-not  in Glasgow Haskell?

I currently think that  `abstract'  is a tool related to unfolding. 
And in Glasgow Haskell it is called `inlining'.
Do I undertsand cor

Re: `abstract' on Web keywords

Nils Anders Danielsson — 2013-05-15T08:58:53

If you use abstract, then the type signature is "frozen" before the body
is checked. This can be annoying, but ensures that implementation
details do not leak out. In your case I guess you do not care about such
leakage, because you use abstract for performance reasons, not to hide
implementation details. One possibility is to have two kinds of
abstract, one that is aimed at performance and one that is aimed at
information hiding. However, abstract is already a bit of a hack.

Re: `abstract' on Web keywords

Sergei Meshveliani — 2013-05-14T16:11:01



Probably, I have confused things.
It needs to be said
"Because checking any function  f  outside of the abstract scope does
not need to unfold inside f the body of the this abstracted function".

Regards,

------
Sergei

RDP 2013 Call for Participation

Luca Paolini — 2013-05-14T07:53:45

*********************************************************************
*** Federated Conference on Rewriting, Deduction, and Programming ***
***                            RDP 2013                           ***
***                    June 23 - June 28, 2013                    ***
***                   Eindhoven, The Netherlands                  ***
***                 http://www.win.tue.nl/rdp2013/                ***
***                                                               ***
***                     CALL FOR PARTICIPATION                    ***
***                                                               ***
*********************************************************************


*************   EARLY REGISTRATION CLOSES ON JUNE 1     *************

---------------------------------------------------------------------

Re: `abstract' on Web keywords

Sergei Meshveliani — 2013-05-14T10:38:44

1. I have searched through the two manuals, and have not found any
`abstract' (I skip the expressions like "to abstract over").   

2. I have searched in  lib-0.7/src
(not all, though)
and have found only 4 abstract decls -- in BoundedVec*, as I recall.

3. I thought that in my application almost all lemma proofs can be
abstracted. Because other parts are not likely to analyze the structure
of the corresponding proof data (they could, but I do not see a reason
for arranging this in these particular cases).
But I may have a wrong idea about `abstract'.

Now, the obstacle is that all these lemmata are not at the top level,
they are each inside its parametrized module, and usually, somewhere at
the second level of `where'. And abstracting them out most often leads
to "unsolved metas" at the type check. 

One of such attempt has even lead to the checker hung for 30 minutes.  

Another attempt of abstracting out a couple of middle size proofs in 
one module (which takes most of the space in type check) has lead

Re: `abstract' on Web keywords

Nils Anders Danielsson — 2013-05-14T09:22:32

I don't think there is much documentation of abstract in the
(incomplete) reference manual.