Peter Achten | 19 Dec 17:48 2014
Picon

[TFP2015] 1st call for papers

                         -----------------------------
                         C A L L   F O R   P A P E R S
                         -----------------------------

                         ======== TFP 2015 ===========

               16th Symposium on Trends in Functional Programming
                                June 3-5, 2015
                        Inria Sophia Antipolis, France
                           http://tfp2015.inria.fr/

The symposium on Trends in Functional Programming (TFP) is an
international forum for researchers with interests in all aspects of
functional programming, taking a broad view of current and future
trends in the area. It aspires to be a lively environment for
presenting the latest research results, and other contributions (see
below). Authors of draft papers will be invited to submit revised
papers based on the feedback receive at the symposium.  A
post-symposium refereeing process will then select a subset of these
articles for formal publication.

The selected revised papers are expected to be published as a Springer
Lecture Notes in Computer Science (LNCS) volume.

TFP 2015 will be the main event of a pair of functional programming
events. TFP 2015 will be accompanied by the International Workshop on
Trends in Functional Programming in Education (TFPIE), which will take
place on June 2nd.

The TFP symposium is the heir of the successful series of Scottish
(Continue reading)

Peter Selinger | 18 Dec 19:06 2014
Picon
Picon

termination checking

I have a question about termination checking. The following example
has been vexing me. I do not understand why the function
RecordExample.div-aux fails termination checking, while both
RecordExample.fibonacci and DataTypeExample.div-aux pass it.

Agda version 2.4.2.2. Might this be a subtle bug in the termination
checker with respect to inductive records? Or is there something
obvious that I am missing.

Any help appreciated! Thanks, -- Peter

P.S.: although the example works if I use a datatype, I prefer using a
record, because then I can use the constructor in let-bindings, and
also when matching against irrelevant arguments. In the case of
datatypes, these two kinds of pattern matches are not allowed.

----------------------------------------------------------------------
open import Data.Nat
open import Relation.Nullary

module TerminationExample where

-- Some true lemmas about natural numbers. Proofs omitted for brevity.
postulate
  lemma-refl : ∀ n -> n ≤ n
  lemma-suc : ∀ n -> n ≤ suc n
  lemma-order : ∀ {n m} -> ¬ n ≤ m -> n > 0
  lemma-minus : ∀ n m -> n > 0 -> n ∸ suc m < n

module RecordExample where
(Continue reading)

Johan Jeuring | 18 Dec 08:48 2014
Picon

CFP: TFPIE 2015

      Trends in Functional Programming in Education (TFPIE 2015)
                          Call for papers
             https://wiki.science.ru.nl/tfpie/TFPIE2015

The 4th International Workshop on Trends in Functional Programming in Education,
TFPIE 2015, will be held on June 2, 2015 in Sophia-Antipolis in France. It is
co-located with the Symposium on Trends in Functional Programming (TFP 2015)
which takes place from June 3 - 5.

*** Goal ***

The goal of TFPIE is to gather researchers, teachers and professionals that use,
or are interested in the use of, functional programming in education. TFPIE aims
to be a venue where novel ideas, classroom-tested ideas and work-in-progress on
the use of functional programming in education are discussed. The one-day
workshop will foster a spirit of open discussion by having a review process for
publication after the workshop. The program chair of TFPIE 2015 will screen
submissions to ensure that all presentations are within scope and are of
interest to participants. Potential presenters are invited to submit an extended
abstract (4-6 pages) or a draft paper (up to 16 pages) in EPTCS style. The
authors of accepted presentations will have their preprints and their slides
made available on the workshop's website/wiki. Visitors to the TFPIE 2015
website/wiki will be able to add comments. This includes presenters who may
respond to comments and questions as well as provide pointers to improvements
and follow-up work. After the workshop, presenters will be invited to submit (a
revised version of) their article for review. The PC will select the best
articles for publication in the journal Electronic Proceedings in Theoretical
Computer Science (EPTCS). Articles rejected for presentation and extended
abstracts will not be formally reviewed by the PC. TFPIE workshops have
previously been held in St Andrews, Scotland (2012), Provo Utah, USA (2013), and
(Continue reading)

Kenichi Asai | 16 Dec 15:55 2014
Picon

How can I prove associativity of vectors?

I think this is FAQ, but I could not find the answer.  How can I prove
associativity of vectors?  If I write:

assoc : forall {a l m n} {A : Set a} ->
        (l1 : Vec A l) -> (l2 : Vec A m) -> (l3 : Vec A n) ->
        (l1 ++ l2) ++ l3 == l1 ++ (l2 ++ l3)
assoc l1 l2 l3 = ?

even the type doesn't type check, because left-hand side has a type
Vec A ((l + m) + n) while right-hand side Vec A (l + (m + n)).
It appears I need a way to identify these two types.  Could somebody
help?

Thank you in advance.

Sincerely,

--

-- 
Kenichi Asai
module Append where

open import Data.Nat
open import Data.Vec hiding (_++_)
open import Relation.Binary.PropositionalEquality

_++_ : ∀ {a m n} {A : Set a} → Vec A m → Vec A n → Vec A (m + n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
(Continue reading)

Thorsten Altenkirch | 16 Dec 14:19 2014
Picon
Picon

PhD studentship on Homotopy Type Theory in Nottingham

We have a PhD place on a HoTT related topic – please apply or spread the word.

Sorry for the tight deadline – this way an international candidate would have enough time to apply for additional funding via the international office.

Short-listing will take place in January – interviews will be either in person or via Skype. A possible start date is October 2015, but earlier dates are possible.

Thorsten

PhD Studentship - Homotopy Type Theory related topic in the Functional Programming Laboratory

ReferenceSCI1420Closing DateFriday, 16th January 2015DepartmentComputer Science - Functional Programming Laboratory

Homotopy Type Theory related topic in the Functional Programming Laboratory at University of Nottingham 

Supervisor: Dr Thorsten Altenkirch

We invite applications for a PhD student to work on topics related to the the recently funded EPSRC grant "Homotopy Type Theory: Programming and Verification" obtained by Professor Neil Ghani and Dr Conor McBride (University of Strathclyde), Dr Thorsten Altenkirch (University of Nottingham) and Dr Nicola Gambino (University of Leeds).

Homotopy Type Theory (HoTT) is a revolutionary new approach to type theory where types are interpreted as spaces, terms as points and equalities as paths. Decades of research in homotopy theory has uncovered the structure of such paths and HoTT uses this structure as the basis of a new theory of equality. Excitingly, within homotopy theory, one naturally studies higher homotopies of paths between paths and this gives the higher dimensional structure of equality we previously lacked. The objective of this grant is to translate the advances of HoTT into more concrete programming language and verification tools.

The prospective student should have a background in Computer Science and/or Mathematics and have a keen interest in logic, foundations of Computer Science and Mathematics and Programming Languages. A good knowledge of functional programming is helpful. Successful applicants should have completed (or will complete soon) an MSc with a (predicted) first class classification or comparable. Good communication skills and the ability to work with the thriving group in Nottingham and to interact with our colleagues in Strathclyde and Leeds are important assets.

The studentship will cover PhD tuition fees and a tax free stipend for three years (£13,590 for the 2014-15 academic year) for UK/EU students. For international students it is possible to apply for additional funding via the University of Nottingham to bridge the difference but this is subject to tight deadlines and an additional selection process. Funding is for 3 years, completion of PhD has to happen within 4 years.

Applicants should email Thorsten.Altenkirch-QabDm/c3fAmwa9SdKMSz+Q@public.gmane.org with:

  • an up-to-date CV, including the email addresses of 1 - 2 relevant  academic references; 
  • transcript and/or certificates (scanned);
  • a short (1 - 2 pages) research proposal;
  • 1-2 examples of their work (eg slides of talks, projects, thesis) in electronic form; and
  • a cover letter (or email) explaining their reasons to apply for this position (< 500 words).
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
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Wolfram Kahl | 15 Dec 17:15 2014
Picon
Picon

Re: proofs with "with"

Hallo Peter,

On Mon, Dec 15, 2014 at 01:27:26AM -0400, Peter Selinger wrote:
> This is a newbie question. I am being driven mad by proofs about
> definitions that use the "with" notation.

My pragmatic suggestion: Don't!  ;-)

That is, it usually makes your life easier if you don't use "with"
in definitions that you later will want to prove something about.

The "with" notation just generates an auxiliary function;
it is usually only a minor nuisance to generate that function yourself.

(Sometimes, Function.case_of_ with a pattern-matching lambda
 is also an alternative (with the disadvantage that the auxiliary function
 does not have a name of your choice).
)

Wolfram

P.S.: If you redo your example with Data.Product from the standard library,
  then

> -- Return a natural number not in L.
> newNat : (L : List Nat) -> Nat
> newNat L with theorem-infinite L
> newNat L | ([ n , p ]) = n

becomes

newNat L = proj_1 (theorem-infinite L)
Peter Selinger | 15 Dec 06:27 2014
Picon
Picon

proofs with "with"

This is a newbie question. I am being driven mad by proofs about
definitions that use the "with" notation. The situation is typically
like this:

lemma : A -> B
lemma x with expr
lemma x | y = ?

Within the proof context '?', a variable y is available, of the same
type as expr. However, often, to complete the proof, one has to use
the fact that y == expr. This fact is obviously true, but typically
does not follow from anything in the proof context.

The "rewrite" notation does not help here, because its purpose is to
use an equation, not to prove one. 

Here is a concrete example (full definitions and proofs appended
below). I have defined an operation for computing the maximum of a
list of natural numbers:

maximum : (L : List Nat) -> Nat

I have also proved a lemma showing that the maximum is indeed an upper
bound for the list:

lemma-maximum : (L : List Nat) -> ∀ m -> m ∈ L -> m <= maximum L

One can then easily prove a theorem stating that there are infinitely
many natural numbers:

theorem-infinite : (L : List Nat) -> ∃[ n ∈ Nat ] (n ∉ L)

Since existential witnesses are not very convenient to use, I'd like
to split this theorem into a first and second component: the first
component is a function computing a natural number not in a given
list, and the second component is the lemma saying that the number is
indeed not in the list:

-- Return a natural number not in L.
newNat : (L : List Nat) -> Nat
newNat L with theorem-infinite L
newNat L | ([ n , p ]) = n

-- The defining property of newNat.
lemma-newNat : (L : List Nat) -> newNat L ∉ L
lemma-newNat L with theorem-infinite L
lemma-newNat L | ([ n , p ]) = ?

However, I cannot complete the last proof. In principle, the question
mark should just be "p". However, the prover (modulo beta reduction)
serves

Goal: newNat L ∉ L

as the goal, and gives

p : n ∉ L
n : Nat
L : List Nat

as the hypotheses. Obviously, [ n , p ] was obtained by pattern
matching theorem-infinite L, so we know that

[ n , p ] == theorem-infinite L.

>From this, we could immediately conclude that newNat L == n, which
would immediately prove the goal. But I have not been able to find any
combination of dot-patterns that the type checker would actually
accept.

Two questions:

(1) what is the concrete solution to my problem?

   I realize that I can solve the problem by defining general first
   and second projections from the existential type:

   ∃fst : {A : Set} {B : A -> Set} -> ∃[ x ∈ A ] B x -> A
   ∃snd : {A : Set} {B : A -> Set} -> (p : ∃[ x ∈ A ] B x) -> B (∃fst p) 

   and then I can just define newNat and lemma-newNat in terms of
   these. However, I am more concerned with what one can do when one
   is stuck in a proof context, rather than such an "external"
   solution to the problem.

(2) why doesn't Agda do the obvious, namely, when matching a "with"
    expression "expr" against a pattern "p", just add the equation
    "expr == p" to the proof context? Is there an existing mechanism
    that can achieve this?

Thanks, -- Peter

Here's the full example. It requires no libraries.

module InfNat where

-- Falsity.
data False : Set where
  -- no constructors.

-- Negation.
Not : Set -> Set
Not A = A -> False

-- Existential quantifier.
data Exists (A : Set) (B : A -> Set) : Set where
  [_,_] : (a : A) -> B a -> Exists A B
syntax Exists A (λ x -> B) = ∃[ x ∈ A ] B

-- The natural numbers.
data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

-- Order.
data _<=_ : Nat -> Nat -> Set where
  z<=n : ∀ {n} → zero <= n
  s<=s : ∀ {m n} (m<=n : m <= n) → succ m <= succ n

-- Order is reflexive.
lemma-order-refl : ∀ {n} -> n <= n
lemma-order-refl {zero} = z<=n
lemma-order-refl {succ n} = s<=s lemma-order-refl

-- Order is transitive.
lemma-order-trans : ∀ {n m k} -> n <= m -> m <= k -> n <= k
lemma-order-trans z<=n q = z<=n
lemma-order-trans (s<=s p) (s<=s q) = s<=s (lemma-order-trans p q)

-- Successor is not smaller.
lemma-order-succ : ∀ {n} -> Not (succ n <= n)
lemma-order-succ (s<=s h) = lemma-order-succ h

-- The maximum of two numbers.
max : Nat -> Nat -> Nat
max zero m = m
max n zero = n
max (succ n) (succ m) = succ (max n m)

-- Introduction rules for maximum.
lemma-max-intro1 : ∀ n m -> n <= max n m
lemma-max-intro1 zero m = z<=n
lemma-max-intro1 (succ n) zero = lemma-order-refl
lemma-max-intro1 (succ n) (succ m) = s<=s (lemma-max-intro1 n m)

lemma-max-intro2 : ∀ n m -> m <= max n m
lemma-max-intro2 zero m = lemma-order-refl
lemma-max-intro2 (succ n) zero = z<=n
lemma-max-intro2 (succ n) (succ m) = s<=s (lemma-max-intro2 n m)

-- Lists.
data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A

-- Membership.
data _∈_ {A : Set} (x : A) : (B : List A) -> Set where
  mem-head : {xs : List A} -> x ∈ (x :: xs)
  mem-tail : {xs : List A} {y : A} -> x ∈ xs -> x ∈ (y :: xs)

-- Not member.
_∉_ : {A : Set} -> (x : A) -> (B : List A) -> Set 
x ∉ B = Not (x ∈ B)

-- Calculate the maximum of a list of numbers.
maximum : (L : List Nat) -> Nat
maximum [] = zero
maximum (n :: L) = max n (maximum L)

-- The maximum is an upper bound.
lemma-maximum : (L : List Nat) -> ∀ m -> m ∈ L -> m <= maximum L
lemma-maximum (n :: L) .n mem-head = lemma-max-intro1 n (maximum L)
lemma-maximum (n :: L) m (mem-tail p) = lemma-order-trans (lemma-maximum L m p) (lemma-max-intro2 n
(maximum L))

-- Theorem: there are infinitely many natural numbers.
theorem-infinite : (L : List Nat) -> ∃[ n ∈ Nat ] (n ∉ L)
theorem-infinite L = [ n , p ]
  where
    n = succ (maximum L)
    p : n ∉ L
    p h = let q = lemma-maximum L n h in lemma-order-succ q

-- Return a natural number not in L.
newNat : (L : List Nat) -> Nat
newNat L with theorem-infinite L
newNat L | ([ n , p ]) = n

-- The defining property of newNat.
lemma-newNat : (L : List Nat) -> newNat L ∉ L
lemma-newNat L with theorem-infinite L
lemma-newNat L | ([ n , p ]) = {!!}
Philipp Hausmann | 12 Dec 15:47 2014
Picon

Example Runnable Agda Programs

Hi,

I am looking for example programs to test the Agda compilers. Just by
searching github, google & co I couldn't find many Agda programs which
can actually be run and do something interesting.

To give a bit of context, we are working on a new backend for Agda and
would like to have some regression tests. We have some simple
HelloWorld-style programs. but we are missing some more complicated
examples. Currently we are porting the Eliza [1] example from GHC's
nofib testsuite, but adding already existing Agda programs would be much
less work....  Especially interesting would also be examples where the
current MAlonzo backend fails or produces bad code. I remember seeing
some emails about them on the mailing list [2, 3, 4], but I don't
remember seeing any actual code example for reproducing these errors.

As the behaviour of Agda programs should not really depend on the
backend, I think the test programs would be useful for the MAlonzo
backend as well.

Long story short, does anyone have actual runnable Agda programs we
could use for testing?

Cheers,
Philipp

[1]
https://github.com/phile314/agda/blob/compiler-tests/test/exec/with-stdlib/Eliza.agda
[2] https://lists.chalmers.se/pipermail/agda/2012/004423.html
[3] https://lists.chalmers.se/pipermail/agda/2013/005229.html
[4] https://lists.chalmers.se/pipermail/agda/2014/006990.html
edprocess | 11 Dec 11:38 2014

CFP: ICADIWT 2015 at Hong Kong


Sixth International Conference on the Applications of Digital  
Information and Web Technologies (ICADIWT 2015)
February 10-12, 2015
Macau and Hongkong.
(www.socio.org.uk/icadiwt)
Springer CCIS (pending approval)

The Sixth International Conference on the Applications of Digital  
Information and Web Technologies (ICADIWT 2015) is a forum for  
scientists, engineers, and practitioners to present their latest  
research results, ideas, developments and applications in the areas of  
Computer Communications, Communication networks, Communication  
Software Communication Technologies and Applications, and other  
related themes.

This conference (ICADIWT Edition VI) will include presentations of  
contributed papers and state-of-the-art lectures by invited keynote  
speakers.

This conference welcomes papers address on, but not limited to, the  
following research topics:

Internet Communication
Internet Technologies
Web Applications
Internet Software
Data Access and Transmission
Digital Communication Software
Digital Networks
Digital Communication Software
Internet Content Processing
Internet of Things
Internet of Everything
Data Communication
Databases and applications
Web Systems Engineering Design
Intelligent Agent systems
Semantic Web Studies
Adaptive Web applications and personalization
Navigation and hypermedia

The accepted full papers will be published in the conference  
proceedings (Springer CCIS) and submitted for inclusion in many  
indexes. Accepted full papers will be submitted for indexing to  
multiple abstract and indexing partners.

Selected papers after modification will be published in the following  
reviewed journals.

Journal of Computer and System Sciences/ (ISI/Scopus)
Journal of Digital Information Management (Scopus/EI)
International Journal of Computational Science and Engineering (Scopus  
and EI Indexed)
Decision Analytics
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 Strategic Decision Sciences
International Journal of Enterprise Information Systems (Scopus/EI)

Important Dates

Submission of papers	December 25, 2014
Notification of Acceptance/Rejection	January 15 2015
Camera ready	February 05, 2015
Registration early bird	January 25 2015
Registration late	January 31 2015
Conference dates	February 10-12 2015

Email: icadiwt@...
Submissions at http://www.socio.org.uk/icadiwt/paper-submission/
----------------
Mateusz Kowalczyk | 10 Dec 01:43 2014
Picon

Re: Agda and Emacs mode

On 12/10/2014 12:37 AM, Mateusz Kowalczyk wrote:
> On 12/09/2014 11:27 AM, Andrej Bauer wrote:
>> I have a master's student who would like to write a GUI for Agda on
>> OSX (well, was told to do so).
>>
>> I suggested that he should just hook into Agda's communication with
>> Emacs. Is there reasonable documentation on how Agda communicates with
>> Emacs?
>>
>> Also, he now tells me that the Agda executable presupposes the
>> existence of Emacs, which I have a hard time believing.
>>
>> Can someone shed some light on how realistic a project this is?
>>
>> With kind regards,
>>
>> Andrej
>> _______________________________________________
>> Agda mailing list
>> Agda@...
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
> 
> Some investigation was done
> 

Apologies, didn't mean to send that, damn Thunderbird.

What I was going to say is that there was some investigation done into
these commands by previous project (for the Atom editor I believe) but I
can't find the file now. I started to do ‘the emacs way’ of talking to
the process in Yi but it's very quickly becoming cumbersome. If your
student is going to use Haskell, I recommend he does what Andreas
recommended to me some weeks ago: collect the functions we want Agda to
expose and try to establish an API proper, maintaining it between Agda
releases.

--

-- 
Mateusz K.
Andrej Bauer | 9 Dec 12:27 2014

Agda and Emacs mode

I have a master's student who would like to write a GUI for Agda on
OSX (well, was told to do so).

I suggested that he should just hook into Agda's communication with
Emacs. Is there reasonable documentation on how Agda communicates with
Emacs?

Also, he now tells me that the Agda executable presupposes the
existence of Emacs, which I have a hard time believing.

Can someone shed some light on how realistic a project this is?

With kind regards,

Andrej

Gmane