Roman | 23 Jul 19:19 2016
Picon

How to show a Term?

Hi. `unquote` allows to print a Term, but it also performs type
checking. Is there a way to print a Term just like `unquote` does, but
without type checking it? I.e. something like `showTerm : Term ->
String`. It's hard to read plain Terms even with appropriate {-#
DISPLAY #-} pragmas and more importantly we could define a type class

record Quote {α} (A : Set α) : Set α where
  field deepQuote : A -> Term

  show : A -> String
  show = showTerm ∘ deepQuote
open Quote {{...}} public

instead of the Show type class and delegate pretty printing to the
built-in machinery therefore avoiding all the burden of dealing with
associativity, inserting parentheses and spaces etc.
Guillermo Calderon | 21 Jul 21:04 2016
Picon

instance candidates in record fields


Hi;

I have a problem working with instance arguments in Agda 2.5.1

Here is a simplified code to illustrate the problem:

----------------------------------------------
-- my class
record MyClass  : Set₁ where
   field
    C  : Set
    op : C → C → C
    eq : C → C → Set

-- a record using MyClass
record Q (CA CB : MyClass) : Set where

   open MyClass ⦃...⦄
   instance fooA = CA
            fooB = CB

   A = MyClass.C CA
   B = MyClass.C CB

  field
     f : A → B
     prop : ∀ {a b} → eq a b → eq (f a) (f b)
               ^^^    ^^^^^^
                (yellow)
(Continue reading)

Roman | 20 Jul 10:57 2016
Picon

Why does Agda think this is not strictly positive?

Hi. Here is the code:

    open import Level

    data Coerce β : ∀ {α} -> Set α -> Set β where
      coerce : ∀ {A} -> A -> Coerce β A

    data D : Set where
      C : Coerce zero D -> D

Agda reports

    D is not strictly positive, because it occurs
    in the third argument to Coerce
    in the type of the constructor C
    in the definition of D.

Is Agda correct that D is not strictly positive? Is there something I
can do to make positivity check pass?
Lindsey Kuper | 19 Jul 07:43 2016

Call for Participation: ICFP 2016


[ Early registration ends 17 August. ]

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

Call for Participation

ICFP 2016
21st ACM SIGPLAN International Conference on Functional Programming
and affiliated events

September 18 - September 24, 2016
Nara, Japan
http://conf.researchr.org/home/icfp-2016

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

ICFP provides a forum for researchers and developers to hear
about the latest work on the design, implementations, principles, and
uses of functional programming. The conference covers the entire
spectrum of work, from practice to theory, including its peripheries.

A full week dedicated to functional programming:
1 conference, 1 symposium, 10 workshops, tutorials,
programming contest results, student research competition,
and mentoring workshop

* Overview and affiliated events:
  http://conf.researchr.org/home/icfp-2016

(Continue reading)

Sergei Meshveliani | 15 Jul 21:35 2016
Picon

problem with `abstract'

Dear Agda developers,

the following usage of `abstract' is not type-checked in 
Agada 2.5.1.1 + ghc-7.10.2 : 

-----------------------------------------------------------------------
open import Relation.Binary using () renaming (Decidable to Decidable₂)
open import Data.Product    using (_×_; proj₂)
open import Data.List       using (List; map)
open import Data.List.All   using (All) 
open import Data.Nat as Nat using (ℕ; _<_)

-- of appliaction --       
open import Structures0 using (Magma)
open import Structures3 using (UpIntegralRing)
open import Structures7 using (module OverIntegralRing-3)

abstract 
 f : ∀ {α α=} → 
     (upIR : UpIntegralRing α α=) → 
     (open UpIntegralRing upIR using (Carrier; 1#; *magma))
     (_∣?_ : Decidable₂ (Magma._∣_ *magma)) →  
     (open OverIntegralRing-3 upIR _∣?_ using (Factorization))   

     (a : Carrier) → Factorization a → Carrier 

 f {α} {_} upIR _∣?_ a ft =  g (ftPairs ft) (exps>0 ft)
   where
   open UpIntegralRing     upIR      using (Carrier; 1#)        
   open OverIntegralRing-3 upIR _∣?_ using (Factorization)
(Continue reading)

Peter Selinger | 6 Jul 21:03 2016
Picon
Picon

origin of "Agda"?

Does anyone know why Agda is called Agda? I realize the name is based
on the 1999 "Agda 1" by Catarina Coquand, but what was the meaning of
the original name? Is it an acronym (I noticed that some of the early
papers spell it AGDA)? Or is it someone's name? I looked at some of
the Agda 1 materials, but found no explanation.

Just curious, -- Peter
publicityifl | 5 Jul 12:17 2016
Picon

2nd CfP: IFL 2016 (28th Symposium on Implementation and Application of Functional Languages)

Hello,

Please, find below the second call for papers for IFL 2016.
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

---

IFL 2016 - 2nd Call for papers

28th SYMPOSIUM ON IMPLEMENTATION AND APPLICATION OF FUNCTIONAL LANGUAGES - IFL 2016

KU Leuven, Belgium

In cooperation with ACM SIGPLAN

August 31 - September 2, 2016

https://dtai.cs.kuleuven.be/events/ifl2016/

Scope

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 2016 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 programming.

Peer-review

Following the IFL tradition, IFL 2016 will use a post-symposium review process
to produce the formal proceedings. All participants of IFL 2016 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:

http://www.sigplan.org/Resources/Policies/Republication

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 are not subject to 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. The formal proceedings will appear in the
International Conference Proceedings Series of the ACM Digital Library.

Important dates

August 1: Submission deadline draft papers
August 3: Notification of acceptance for presentation
August 5: Early registration deadline
August 12: Late registration deadline
August 22: Submission deadline for pre-symposium proceedings
August 31 - September 2: IFL Symposium
December 1: Submission deadline for post-symposium proceedings
January 31, 2017: Notification of acceptance for post-symposium proceedings
March 15, 2017: Camera-ready version for post-symposium proceedings

Submission details

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 use the new ACM two
columns conference format, which can be found at:

http://www.acm.org/publications/proceedings-template

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.

Authors submit through EasyChair:

https://easychair.org/conferences/?conf=ifl2016

Topics

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 2016,
please contact the PC chair at tom.schrijvers-4rd9VHyGk8h2kGVRwRwAbw@public.gmane.org. Topics of interest include,
but are not limited to:

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

Chair: Tom Schrijvers, KU Leuven, Belgium

- Sandrine Blazy, University of Rennes 1, France
- Laura Castro, University of A Coruña, Spain
- Jacques, Garrigue, Nagoya University, Japan
- Clemens Grelck, University of Amsterdam, The Netherlands
- Zoltan Horvath, Eotvos Lorand University, Hungary
- Jan Martin Jansen, Netherlands Defence Academy, The Netherlands
- Mauro Jaskelioff, CIFASIS/Universidad Nacional de Rosario, Argentina
- Patricia Johann, Appalachian State University, USA
- Wolfram Kahl, McMaster University, Canada
- Pieter Koopman, Radboud University Nijmegen, The Netherlands
- Shin-Cheng Mu, Academia Sinica, Taiwan
- Henrik Nilsson, University of Nottingham, UK
- Nikolaos Papaspyrou, National Technical University of Athens, Greece
- Atze van der Ploeg, Chalmers University of Technology, Sweden
- Matija Pretnar, University of Ljubljana, Slovenia
- Tillmann Rendel, University of Tübingen, Germany
- Christophe Scholliers, Universiteit Gent, Belgium
- Sven-Bodo Scholz, Heriot-Watt University, UK
- Melinda Toth, Eotvos Lorand University, Hungary
- Meng Wang, University of Kent, UK
- Jeremy Yallop, University of Cambridge, UK

Venue

The 28th IFL will be held in association with the Faculty of Computer Science,
KU Leuven, Belgium. Leuven is centrally located in Belgium and can be easily
reached from Brussels Airport by train (~15 minutes). The venue in the
Arenberg Castle park can be reached by foot, bus or taxi from the city center.
See the website for more information on the venue.

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Guillermo Calderon | 28 Jun 20:27 2016
Picon

Formalization of Linear Algebra in agda

Dear all,

I am looking for a formalization  in Agda
of vectorial spaces (over a field).
My concern is to work in the formalization of some concepts involved 
with Grassman and Clifford algebras which are defined as extensions of
vectorial spaces.

I would be very grateful if anyone can give me some references on this 
topic.

Thanks,

Guillermo
Ren Rise | 24 Jun 23:14 2016
Picon

Re: help required for installing GHC or whole Haskell platform

Please see below my perpetual efforts to get Agda installed on my Windows 10 workstation and to start exploring Agda is resulting in failures after failures over the last 7-8 days.
Please come to my aid. I am not one to give up, never until I get what I want. 
 
C:\Users\SurajZ>cd C:\Program Files\Haskell Platform
C:\Program Files\Haskell Platform>cabal install agda2
Warning: C:\Users\SurajZ\AppData\Roaming\cabal\config: Unrecognized stanza on
line 14
Warning: No remote package servers have been specified. Usually you would have
one specified in the config file.
cabal: There is no package named 'agda2'.
You may need to run 'cabal update' to get the latest list of available
packages.
C:\Program Files\Haskell Platform>cabal update
Warning: C:\Users\SurajZ\AppData\Roaming\cabal\config: Unrecognized stanza on
line 14
Warning: No remote package servers have been specified. Usually you would have
one specified in the config file.
C:\Program Files\Haskell Platform>cabal install Agda
Warning: C:\Users\SurajZ\AppData\Roaming\cabal\config: Unrecognized stanza on
line 14
Warning: No remote package servers have been specified. Usually you would have
one specified in the config file.
cabal: There is no package named 'Agda'.
You may need to run 'cabal update' to get the latest list of available
packages.
C:\Program Files\Haskell Platform>
 
Sent: Friday, June 24, 2016 at 12:02 AM
From: "Oleg Lobachev" <lobachev <at> Mathematik.Uni-Marburg.de>
To: "Ren Rise" <ren.rise <at> gmx.com>
Subject: Re: [Agda] help required for installing GHC or whole Haskell platform
Not cabal install, but cabal install agda2 or how it was again. 

Sent from my iPhone

On 22.06.2016, at 07:53, Ren Rise <ren.rise <at> gmx.com> wrote:
 
I have just downloaded cabal by running cabal update. Please see the followins lines from my command prompt: 
 
C:\Program Files\Haskell Platform>cabal update
Downloading the latest package list from hackage.haskell.org
 
But when I run cabal install, it again throws up exceptions:
 
C:\Program Files\Haskell Platform>cabal install
cabal: Error reading local package.
Couldn't find .cabal file in: .
C:\Program Files\Haskell Platform>
 
Now what do I do?
 
Sent: Wednesday, June 22, 2016 at 9:49 AM
From: "Andrés Sicard-Ramírez" <asr <at> eafit.edu.co>
To: "Ren Rise" <ren.rise <at> gmx.com>
Subject: Re: [Agda] help required for installing GHC or whole Haskell platform
On 21 June 2016 at 23:08, Ren Rise <ren.rise <at> gmx.com> wrote:
> C:\Program Files\Haskell Platform>cabal install Agda
> 'cabal' is not recognized as an internal or external command,

The cabal program is not in your path.


--
Andrés
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.
_______________________________________________
Agda mailing list
Agda <at> lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Jeremy Yallop | 23 Jun 10:18 2016
Picon

PEPM 2017 Call for Papers

CALL FOR PAPERS
Workshop on PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM 2017)

http://conf.researchr.org/home/PEPM-2017

Paris, France, January 16th - 17th, 2017
(co-located with POPL 2017)

PEPM is the premier forum for discussion of semantics-based program
manipulation.  The first ACM SIGPLAN PEPM symposium took place in
1991, and meetings have been held in affiliation with POPL every year
since 2006.

PEPM 2017 will be based on a broad interpretation of semantics-based
program manipulation, reflecting the expanded scope of PEPM in recent
years beyond the traditionally covered areas of partial evaluation and
specialization.  Specifically, PEPM 2017 will include practical
applications of program transformations such as refactoring tools, and
practical implementation techniques such as rule-based transformation
systems.  In addition, the scope of PEPM covers manipulation and
transformations of program and system representations such as
structural and semantic models that occur in the context of
model-driven development.  In order to maintain the dynamic and
interactive nature of PEPM and to encourage participation by
practitioners, we also solicit submissions of short papers, including
tool demonstrations, and of posters.

Scope
-----

Topics of interest for PEPM 2017 include, but are not limited to:

* Program and model manipulation techniques such as: supercompilation,
  partial evaluation, fusion, on-the-fly program adaptation, active
  libraries, program inversion, slicing, symbolic execution,
  refactoring, decompilation, and obfuscation.

* Program analysis techniques that are used to drive program/model
  manipulation such as: abstract interpretation, termination checking,
  binding-time analysis, constraint solving, type systems, automated
  testing and test case generation.

* Techniques that treat programs/models as data objects including
  metaprogramming, generative programming, embedded domain-specific
  languages, program synthesis by sketching and inductive programming,
  staged computation, and model-driven program generation and
  transformation.

* Application of the above techniques including case studies of
  program manipulation in real-world (industrial, open-source)
  projects and software development processes, descriptions of robust
  tools capable of effectively handling realistic applications,
  benchmarking.  Examples of application domains include legacy
  program understanding and transformation, DSL implementations,
  visual languages and end-user programming, scientific computing,
  middleware frameworks and infrastructure needed for distributed and
  web-based applications, embedded and resource-limited computation,
  and security.

This list of categories is not exhaustive, and we encourage
submissions describing applications of semantics-based program
manipulation techniques in new domains.  If you have a question as to
whether a potential submission is within the scope of the workshop,
please contact the programme chairs.

Submission categories and guidelines
------------------------------------

Three kinds of submissions will be accepted: Regular Research Papers,
Short Papers and Posters.

* Regular Research Papers should describe new results, and will be
  judged on originality, correctness, significance and clarity.
  Regular research papers must not exceed 12 pages in ACM Proceedings
  style (including appendix).

* Short Papers may include tool demonstrations and presentations of
  exciting if not fully polished research, and of interesting
  academic, industrial and open-source applications that are new or
  unfamiliar.  Short papers must not exceed 6 pages in ACM Proceedings
  style (including appendix).

* Posters should describe work relevant to the PEPM community, and
  must not exceed 2 pages in ACM Proceedings style.  We invite poster
  submissions that present early work not yet ready for submission to
  a conference or journal, identify new research problems, showcase
  tools and technologies developed by the author(s), or describe
  student research projects.

At least one author of each accepted contribution must attend the
workshop and present the work.  In the case of tool demonstration
papers, a live demonstration of the described tool is expected.
Suggested topics, evaluation criteria, and writing guidelines for both
research tool demonstration papers will be made available on the PEPM
2017 web site.

Student participants with accepted papers can apply for a SIGPLAN PAC
grant to help cover travel expenses and other support.  PAC also
offers other support, such as for child-care expenses during the
meeting or for travel costs for companions of SIGPLAN members with
physical disabilities, as well as for travel from locations outside of
North America and Europe.  For details on the PAC programme, see its
web page.

Publication and special issue
-----------------------------

All accepted papers, short papers and posters included, will appear in
formal proceedings published by ACM Press.  Accepted papers will be
included in the ACM Digital Library.  Authors of selected papers from
PEPM 2016 and PEPM 2017 will also be invited to expand their papers
for publication in a special issue of the journal Computer Languages,
Systems and Structures (COMLAN, Elsevier).

Best paper award
----------------

PEPM 2017 continues the tradition of a Best Paper award.  The winner
will be announced at the workshop.

Submission
----------

Papers should be submitted electronically via HotCRP.

   https://pepm17.hotcrp.com/

Authors using LaTeX to prepare their submissions should use the new
improved SIGPLAN proceedings style, and specifically the
sigplanconf.cls 9pt template.

Important Dates
---------------

For Regular Research Papers and Short Papers:

 * Abstract submission : Tuesday 13th September 2016
 * Paper submission    : Friday 16th September 2016
 * Author notification : Monday 24th October 2016
 * Camera ready        : Monday 28th November 2016

For Posters:

 * Poster submission   : Sunday 30th October 2016
 * Author notification : Friday 10th November 2016
 * Camera ready        : Monday 28th November 2016

PEPM workshop:

 * Workshop            : Monday 16th - Tuesday 17th January 2017

The proceedings will be published 2 weeks pre-conference.

AUTHORS TAKE NOTE: The official publication date is the date the
proceedings are made available in the ACM Digital Library. This date
may be up to two weeks prior to the first day of your conference. The
official publication date affects the deadline for any patent filings
related to published work. (For those rare conferences whose
proceedings are published in the ACM Digital Library after the
conference is over, the official publication date remains the first
day of the conference.).

PEPM'17 Programme Co-Chairs
-------------------

Ulrik Schultz (University of Southern Denmark), ups@...
Jeremy Yallop (University of Cambridge), jeremy.yallop@...
Ren Rise | 22 Jun 23:01 2016
Picon

Fw: Re: Re: help required for installing GHC or whole Haskell platform

 
 
Sent: Thursday, June 23, 2016 at 2:31 AM
From: "Ren Rise" <ren.rise <at> gmx.com>
To: "Andrés Sicard-Ramírez" <asr <at> eafit.edu.co>
Subject: Re: Re: [Agda] help required for installing GHC or whole Haskell platform
where do I install the C Compiler? Into Haskell Platform folder or elsewhere in the C root directory?
 
Sent: Thursday, June 23, 2016 at 1:37 AM
From: "Andrés Sicard-Ramírez" <asr <at> eafit.edu.co>
To: "Ren Rise" <ren.rise <at> gmx.com>
Cc: "Agda users" <agda <at> lists.chalmers.se>
Subject: Re: Re: [Agda] help required for installing GHC or whole Haskell platform
On 22 June 2016 at 14:29, Ren Rise <ren.rise <at> gmx.com> wrote:
> No,I don't have any C compiler installed. If you insist, I can install a C
> compiler.


After installing the C compiler, try to install the old-time library using

cabal install old-time


--
Andrés
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda

Gmane