headers
Carlo Combi | 3 Feb 2004 08:40
Picon

TIME 2004 - extended deadline

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Prolog: papers are solicited from different research areas, dealing with 
  time-related issues. Several topics could be of interest for the TYPES 
community. Among them, I mention here: temporal logics for dynamic data 
types; types for temporal data; type evolution; programming languages 
for temporal representation and reasoning.

NEW SUBMISSION DEADLINE: Feb 12, 2004.

------------------------------------------------
The 11th International Symposium on
TEMPORAL REPRESENTATION AND REASONING

  (TIME 2004)

http://www.greyc.unicaen.fr/time2004

Tatihou, Basse Normandie, France
1-3 July, 2004

The purpose of this symposium is to bring together active researchers 
from distinct research areas involving the representation of, or 
reasoning with, time. As with previous meetings in this respected 
series, one of the main goals of the  TIME symposium will be to bridge 
the gap between theoretical and applied research in temporal 
representation and reasoning. Thus, we especially encourage submissions 
concerning temporal aspects within areas such as Artificial 
Intelligence, Temporal/Spatial Databases and Applications of Temporal 
Logic in Computer Science in order to achieve a multi-disciplinary
(Continue reading)

Permalink | Reply | 0 comments |
headers
Andrei Sabelfeld | 4 Feb 2004 11:45
Picon
Picon

FOSAD2004: Foundations of Security Analysis and Design summer school announcement

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

		** Application Deadline: May 31, 2004 **

	    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	    %                                                   %
	    %          FOURTH INTERNATIONAL SCHOOL ON           %
	    %    FOUNDATIONS OF SECURITY ANALYSIS AND DESIGN    %
	    %   ==============================================  %
	    %                                                   %
	    %                    FOSAD 2004                     %
	    %       http://www.sti.uniurb.it/events/fosad       %
	    %                                                   %
	    %       6-11 September 2004, Bertinoro, Italy       %
	    %                                                   %
	    %          *** Preliminary Announcement ***         %
	    %                                                   %
	    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

General Information
^^^^^^^^^^^^^^^^^^^

Security in computer systems and networks is emerging as one of the most
challenging research areas for the future. The main aim of the school is
to offer a good spectrum of current research in foundations of security,
ranging from programming languages to analysis of protocols, that can be
of help for graduate students, young researchers from academia or industry
that intend to approach the field.
The FOSAD series started in 2000 and last edition was in 2002. This year
the school covers one week (from Monday 6 to Saturday 11, September 2004)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Joe Vanderwaart | 3 Feb 2004 23:15
Picon
Favicon

Paper: Foundational Typed Assembly Language for Grid Computing

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Types readers,

We are pleased to announce the availability of our paper, "Foundational 
Typed Assembly Language for Grid Computing".  The paper focuses on our type 
theory for bounding the CPU usage of mobile code; an abstract is below.

The paper is available for download from
	http://www.cs.cmu.edu/~joev/work.html
(currently the first item in the list of papers there).  As always, 
comments are welcome.

-- Joseph C. Vanderwaart and Karl Crary

--------------------------------------------------------
Foundational Typed Assembly Language for Grid Computing
Joseph C. Vanderwaart and Karl Crary

Abstract:

This report describes a type theory for certified code, called TALT-R, in 
which type safety guarantees cooperation with a mechanism to limit the CPU 
usage of untrusted code.  At its core is the foundational typed assembly 
language TALT, extended with an instruction-counting mechanism, or "virtual 
clock", intended to bound the number of non-yielding instructions a program 
may execute in a row.  The type theory also contains a form of dependent 
refinement that allows reasoning about integer values to be reflected in 
the typing of a program; in particular, the refinement system enables a 
simple but effective dynamic checking scheme for the clock, which we
(Continue reading)

Permalink | Reply | 0 comments |
headers
Thorsten Altenkirch | 5 Feb 2004 14:41
Picon

Midland Graduate School 2004 / APPSEM Spring School 2004

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Midland Graduate School 2004 / APPSEM Spring School 2004
********************************************************
http://www.cs.nott.ac.uk/~txa/mgs/

The Midland Graduate School - APPSEM Spring School is taking place 29 
March - 2 April 2004 in Nottingham at the Jubilee Campus  of Nottingham 
University. We especially invite participants from UK universities and 
from sites participating in the APPSEM working group.

We expect to have some grants for UK students, while APPSEM funds can be 
used to support students from APPSEM affiliated sites.

Foundational courses:

Thorsten Altenkirch  	U Nottingham  	Lambda calculus and types  	
Neil Ghani 		U Leicester 	Category Theory 	
Graham Hutton 		U Nottingham 	Functional Programming 	
Achim Jung 		U Birmingham 	Denotational Semantics 	

Advanced courses:

Sara Kalvala 		U Warwick 	Theorem Proving in Isabelle 	Martin Escardo 	 
U Birmingham 	Topology of data types
Alexander Kurz 		U Leicester 	Stone Duality - The Duality of 		 
           			Syntax and Semantics
Conor McBride 		U Durham 	Dependently Typed Programming 	Uday Reddy 		U 
Birmingham 	Programming logics for dynamic 	
   					data structures
(Continue reading)

Permalink | Reply | 0 comments |
headers
iu3 | 6 Feb 2004 14:45
Picon
Picon
Favicon

SOS 2004: Call for Papers

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

                         Call for Papers

	       Structural Operational Semantics

       http://www.cs.auc.dk/~luca/SOS-WORKSHOP/

          A Satellite Workshop of CONCUR 2004
        30 August, 2004, London, United Kingdom

Aims:

Structural operational semantics (SOS) provides a framework 
for giving operational semantics to programming and specification 
languages.  A growing number of programming languages from 
commercial and academic spheres have been given usable semantic 
descriptions by means of structural operational semantics. 
Because of its intuitive appeal and flexibility, structural 
operational semantics has found considerable application in 
the study of the semantics of concurrent processes.  Moreover, 
it is becoming a viable alternative to denotational semantics 
in the static analysis of programs, and in proving compiler 
correctness.

Recently, structural operational semantics has been successfully 
applied as a formal tool to establish results that hold for classes 
of process description languages. This has allowed for 
the generalization of well-known results in the field of process 
algebra, and for the development of a meta-theory for process calculi
(Continue reading)

Permalink | Reply | 0 comments |
headers
lvigano | 5 Feb 2004 18:45
Picon

CFP: Automated Reasoning for Security Protocols Analysis (ARSPA)

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

			 IJCAR 2004 Workshop W6

				 ARSPA

			Automated Reasoning for
		      Security Protocols Analysis

			University College Cork
			     Cork, Ireland
			  Sunday, July 04, 2004

		  http://www.avispa-project.org/arspa
				    

			***********************
			*** CALL FOR PAPERS ***
			***********************


		  Submission deadline: April 15, 2004

BACKGROUND, AIM AND SCOPE
=========================

  Experience over the last twenty years has shown that, even assuming
perfect cryptography, the design of security protocols (or cryptographic
protocols, as they are sometimes called) is highly error-prone and that
conventional validation techniques based on informal arguments and/or
(Continue reading)

Permalink | Reply | 0 comments |
headers
Geoffrey A. Washburn | 6 Feb 2004 17:57
Favicon

Colimit Construction

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

 Recently, I've come across a intriguing categorical construction, and
 am curious as to whether anyone has an insight into the nature of its
 dual construction.  The following examples will be in the category where
 the objects are types and the arrows lambda-calculus functions.  We will
 ignore specifying the definition of types and terms for the moment.
 Consider the following diagram is contained in the category (note all
 diagrams are in ASCII, so you will need to be using a monospace font):

                         \x:Int.(x < 0)
                   Int ------------------> Bool

 One interesting question we can ask about this diagram is the nature of
 its categorical limit.  It is not immediately obvious, so we can gain
 some intuition by first looking at the limit of the simpler diagram,
 that of just the objects Int and Bool.

                   Int                     Bool

 It is well known that the limit of this diagram is the product type.

                            Int x Bool
                            /        \
                           /          \
                          /            \
                    fst  /              \  snd
                        /                \
                       /                  \
                      /                    \
(Continue reading)

Permalink | Reply | 3 comments |
headers
Christopher A. Stone | 6 Feb 2004 21:18
Favicon

Re: Colimit Construction

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

I am very far from being a category theory expert, but my understanding
is that the limits and colimits can be expressed much more simply.

The limit of the diagram 

          f
   A ---------> B

is the object A, with the arrows being the identity and f rather than
fst and snd.  (This is an exercise in Category Theory for Computer
Science by Barr and Wells.)

And in fact, the suggested limit object  Sigma x:A.S(f(x))  is
isomorphic to A.

So, the colimit of the diagram should just be B, with the arrows being f
and the identity.

Chris

--

-- 
Christopher A. Stone / Assistant Professor              stone@...
Computer Science Department, Harvey Mudd College   www.cs.hmc.edu/~stone
1250 North Dartmouth Avenue, Claremont, CA 91711          (909) 607-8975
Permalink | Reply | 0 comments |
headers
Damiani | 7 Feb 2004 09:27
Picon
Favicon

ITRS'04 - Preliminary Call for Papers

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

---------------------------------------------------------------------
PRELIMINARY CALL FOR PAPERS
Workshop on Intersection Types and Related Systems (ITRS '04)
---------------------------------------------------------------------
University of Turku, Finland
Tuesday, 13 July 2004
http://itrs04.di.unito.it/

Co-located with the Joint Meeting of
ICALP '04, the 31st International Colloquium on
                   Automata, Languages, and Programming 
                   (12 to 16 July 2004)
and
LICS '04, the 19th Login in Computer Science
                 (14 to 17 July 2000)
http://www.math.utu.fi/icalp-lics/
---------------------------------------------------------------------

IMPORTANT DATES/DEADLINES:
  Submission of papers:           Sunday,  11 April  2004
  Notification of acceptance:    Monday,  31 May  2004
  Final version:                        TO BE ANNOUNCED
  Workshop:                           Tuesday, 13 July  2004

OVERALL TOPIC AND FORMAT OF WORKSHOP:
  Types support reliable reasoning in many areas such as programming
  languages, logic, linguistics, etc.  A _polymorphic_ type is one
  that stands for some number of instance types.  The use of type
(Continue reading)

Permalink | Reply | 0 comments |
headers
Kevin S. Millikin | 7 Feb 2004 00:22
Favicon

RE: Colimit Construction

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

I'm also far from a category theory expert.

But I think that the (co)cones of A --> B might still be interesting
according to the following intuition.

Consider instead of negative? = \x.(x < 0), the length function on
lists (because I find it more instructive, I guess, because length is a
more expensive computation).  Then, the limit of

        length       
List -----------> Int

is just List as Christopher Stone noted, but your cone with vertex the
dependent sum represents the linked-list implementation trick of
representing the list by a tuple (i.e., record) of the list itself and a
field holding the length.  This is an optimization if length is asked of
lists often enough.

I think that the intuition behind the cocone you want, for the length
example again, is the optimization trick of postponing computation of
something like length until we're sure that the value will be demanded
(i.e., a thunk, containing the List before it is forced and the length
afterward).

This seems to match the dependent product that you suggested, right?
----
Kevin S. Millikin           Architecture Technology Corporation
Research Scientist          Specialists in Computer Architecture
(Continue reading)

Permalink | Reply | 0 comments |

Gmane