headers
Janis Voigtlaender | 17 Jul 2009 10:39
Picon

PEPM'10 - Call for Papers (Deadline: 6 Oct 09) - Invited Speakers announced

===============================================================
                        CALL FOR PAPERS
                  ACM SIGPLAN 2010 Workshop on
     Partial Evaluation and Program Manipulation (PEPM'10)
                  Madrid, January 18-19, 2010

                   (Affiliated with POPL'10)

          http://www.program-transformation.org/PEPM10
===============================================================

INVITED SPEAKERS:

* Lennart Augustsson (Standard Chartered Bank, UK)
* Jeremy Siek (University of Colorado at Boulder, USA)

IMPORTANT DATES:

* Paper submission:    Tue, October  6, 2009, 23:59, Apia time
* Author notification: Thu, October 29, 2009
* Camera-ready papers: Mon, November 9, 2009

To facilitate smooth organization of the review process, authors are
asked to submit a short abstract by October 1, 2009.

SUBMISSION CATEGORIES:

* Regular research papers (max. 10 pages in ACM Proceedings style)
* Tool demonstration papers (max. 4 pages plus max. 6 pages appendix)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Conor McBride | 7 Apr 2009 15:27
Gravatar

Fwd: JFP Special Issue on Generic Programming

Comrades

Dr Hinze of Oxford requests that I pass on these joyous
tidings to my nearest and dearest. I do so with pleasure.

Cheers

Conor

Begin forwarded message:

> From: Ralf Hinze <ralf.hinze@...>
> Date: 7 April 2009 08:18:28 BST
> To: Conor McBride <conor@...>
> Subject: JFP Special Issue on Generic Programming
>
> PS: Can you also spread the CFP on your local email lists
> and/or among the Dependently-Typed Programming folks.
> Thanks
>
> -------------------------------------------------------------------------------
>
>                             OPEN CALL FOR PAPERS
>
>                   JFP Special Issue on Generic Programming
>
>                           Deadline: 1 October 2009
>
>              http://www.comlab.ox.ac.uk/ralf.hinze/JFP/cfp.html
>
(Continue reading)

Permalink | Reply | 0 comments |
headers
Conor McBride | 13 Mar 2009 11:30
Gravatar

Fwd: Call for papers: Workshop on Termination (WST 2009)

Friends

Janis is visiting Strathclyde at the moment, and has asked me
to pass this along: looks interesting!

Begin forwarded message:

> From: voigt <at> tcs.inf.tu-dresden.de
> Date: 12 March 2009 20:26:51 GMT
> To: conor <at> strictlypositive.org
> Subject: Call for papers: Workshop on Termination (WST 2009)
>
> Hi Conor,
>
> Would you do me the favour of forwarding the below CFP to the Epigram
> mailing list? I think it might be of interest to its readers, as
> termination is an obvious concern in dependently typed languages.
>
> Thanks,
> Janis.
>
> .....................................................................
>
> Tenth International Workshop on Termination (WST 2009)
>
> Leipzig, Germany, June 3-5, 2009
>
> http://www.imn.htwk-leipzig.de/wst09/
>
> Termination is a fundamental topic in computer science. Classical
(Continue reading)

Permalink | Reply | 0 comments |
headers
Thorsten Altenkirch | 13 Mar 2009 11:03
Picon
Gravatar

PhD positions at Nottingham & Swansea

Hi,

we have two fully funded PhD positions in our project on induction- 
recursion: one at Swansea (with Anton Setzer) and one at Nottingham  
(with me). This would be perfect for people who are interested in the  
foundations of Type Theory. See

http://www.cs.nott.ac.uk/~txa/phd.html

Please forward this information to talented students who are looking  
for funding.

Cheers,
Thorsten

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.
Permalink | Reply | 0 comments |
headers
Eric | 22 Sep 2008 19:20

A Text editor for Epigram

Dear all,

As a result of my experiences trying to use Epigram, I would like to 
have a go at writing nicer editor for Epigram programming. I am 
currently studying the "View from the Left" papers and wondered what 
other sources one might consult?

Cheers,
Eric Macalay.
Permalink | Reply | 0 comments |
headers
Thorsten Altenkirch | 30 Jun 2008 12:47
Picon
Gravatar

CFP: Dependently Typed Programming (FI Special Issue)

Hi,

Tarmo and I are editing a special issue on dependently typed  
programming and it would be nice to have papers on Epigram (either on  
the system and its implementation or on applications). So please get  
writing...

It would help with our planning if you could let us know in advance  
whether you plan to submit a paper (let's say end by end of July).

Cheers,
Thorsten & Tarmo

			   Call for Papers:

	       Special Issue of Fundamenta Informaticae
		      (http://fi.mimuw.edu.pl/)
		    Dependently Typed Programming
	 (http://sneezy.cs.nott.ac.uk/darcs/DTP08/journal.html)

			       Editors:
		   Thorsten Altenkirch (Nottingham)
		       Tarmo Uustalu (Tallinn)

Dependently typed programming is using the power of dependent types to
capture relationships between data, internalising invariants necessary
for appropriate computation. When data describe types, we can express
patterns of programming in code. To capture this potential a number of
languages have been proposed and implemented which incorporate some
aspects of dependent types, e.g. Agda, ATS, Cayenne, Coq's CIC,
(Continue reading)

Permalink | Reply | 0 comments |
headers
Serguey Zefirov | 19 Apr 2008 16:37
Picon
Gravatar

And a question on UniqList.

Why there are explicit p:So (...) in

      ( u : A ;  us : UniqList A eq xs ;  p : So (not (elem u xs eq)) !
      !---------------------------------------------------------------!
      !           ulCons u us p : UniqList A eq (cons x xs)           )

?

I, actually, tried to make it implicit, but failed. And I cannot figure why.
Permalink | Reply | 0 comments |
headers
Serguey Zefirov | 19 Apr 2008 15:25
Picon
Gravatar

Why does Epigram colors Branches brown?

     (   X : *    !        ( X : * ;  subs : List (Tup X (Bush X)) !
data !------------!  where !---------------------------------------!
     ! Bush X : * )        !        Branches subs : Bush X         )

Tup is a tuple, List is a list.
Permalink | Reply | 1 comment |
headers
Serguey Zefirov | 21 Mar 2008 17:00
Picon
Gravatar

Equality.

I have type Char = cA | cB | cC | ... | cZ.

If I decide to write charEq (a,b:Char ---- charEq a b:Bool) in
straightforward way, I will be quickly lost in details (26^2
variants).

I tried use of refl, but cannot put it properly: let (a,b:Char; _p :
Eq a b ---- charEq a b _p:Bool) and then use <= case _p does not do
any good to me.

I tried to figure out a type that represents equality in (eq a: EqX a
a) and inequality in some other constructor, but failed.

So the question is: is there any way to express equality like charEq shortly?
Permalink | Reply | 0 comments |
headers
Jacques Carette | 5 Mar 2008 19:30
Picon
Picon
Favicon

CFP: PLMMS 2008

[Two Epigram people are already involved, let's hope for more!]

                          SECOND CALL FOR PAPERS

  * UPDATE: Post-workshop proceedings in Journal of Automated Reasoning
  * UPDATE: Invited talk by Conor McBride

                            Second Workshop on
             Programming Languages for Mechanized Mathematics
                              (PLMMS 2008)

          http://events.cs.bham.ac.uk/cicm08/workshops/plmms/

                        As part of CICM / Calculemus 2008
                     Birmingham, UK, 28-29 July 2008

This workshop is focused on the intersection of programming languages
(PL) and mechanized mathematics systems (MMS). The latter category
subsumes present-day computer algebra systems (CAS), interactive proof
assistants (PA), and automated theorem provers (ATP), all heading
towards fully integrated mechanized mathematical assistants that are
expected to emerge eventually (cf. the objective of Calculemus).

The two subjects of PL and MMS meet in the following topics, which are
of particular interest to this workshop:

  * Dedicated input languages for MMS: covers all aspects of languages
    intended for the user to deploy or extend the system, both
    algorithmic and declarative ones. Typical examples are tactic
    definition languages such as Ltac in Coq, mathematical proof
(Continue reading)

Permalink | Reply | 0 comments |
headers
Serguey Zefirov | 4 Mar 2008 14:11
Picon
Gravatar

wList definition, reloaded.

Being not satisfied with solution I spun from thin air I decided to
reimplement it once again.

If I could invent a type So2 indexed by (Maybe a) type, I could get
the following more appropriate definitions of wNil and wCons (Haskell
style):
wNil = W Nothing notSo2
wCons a as = W (Just a) (lam p => as)

But I cannot get a type, indexed by Maybe:
     ( A : * ;  a : Maybe A !        ( a : A ;  justA : (Just a) !
data !----------------------!  where !---------------------------!
     !      So2 a : *       )        !      oh2 : So2 justA      )

Epigram colors a whole definition in light brown and (Just a) in an
even more brown color. I think it tells me that I am wrong, but I
cannot understand why.

Again.
Permalink | Reply | 2 comments |

Gmane