[Date Prev][Date Next] [Chronological] [Thread] [Top]

[mizar] [gmane.comp.science.types.announce] [Agda] CFP: Dependently Typed Programming (FI Special Issue)

This may be somewhat inappropriate for mizar-forum, but it seems
noteworthy to me that in the non-exhaustive list of systems for
dependent types mentioned in this recent post to the TYPES forum, mizar
is not mentioned.  Would it be appropriate to write an article on
mizar's dependent types for the upcoming special issue of Fundamenta
Informaticae?  One initial question to consider: does mizar's type
system differ in any interesting way from the type sytems mentioned
below?

Jesse
--- Begin Message --- 
[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hi,

Tarmo and I are editing a special issue on dependently typed  
programming and would be peased to see submissions from people on TYPES.

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



			   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,
Concoqtion, DML, Delphin, ELF, Epigram, Omega, OpTT, Pie, PiSigma,  
Ynot for
a non-exhaustive list.

Within the European TYPES project we have organized two workshops to
discuss aspects of dependently programming:

- EffTT, Workshop on Effects and Type Theory
  http://cs.ioc.ee/efftt/
  Tallinn, Estonia, December 2007

- DTP08, Dependently Typed Programming 2008
  http://sneezy.cs.nott.ac.uk/darcs/DTP08/
  Nottingham, UK, February 2008

The special issue is motivated by the desire to give people who have
presented their ideas at those workshops the opportunity to publish
papers on their work. However, we would like to invite everybody
working in this area to submit papers to the special issue. For a more
complete list of topics, please consult the workshop pages following
the links above.

The paper should follow the usual standards of journal papers, and
should be submitted by email (preferable pdf) to one of the editors
before 1 October 2008. We expect that the papers don't exceed 20 pages
(see the FI webpage for style files). We hope to be able to stick to
the following schedule:

	Deadline for submissions:		1 October 08
	Notification of acceptance:		15 January 2009
	Final versions due:			 15 March 2009

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-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org
https://lists.chalmers.se/mailman/listinfo/agda

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.

--- End Message ---

-- 
Jesse Alama (alama@stanford.edu)