Robert Harper | 1 Mar 01:03 2010

[TYPES/announce] University of Oregon Programming Languages Summer School

[ The Types Forum (announcements only), ]

We are pleased to announce this year's program for the University of  
Oregon Programming Languages Summer School, which will be held June  
15-25, 2010 in Eugene, Oregon.  This year's theme is Logic, Languages,  
Compilation, and Verification, and features an impressive roster of  
speakers, including Robert Constable (Cornell), Anupam Datta (Carnegie  
Mellon), Robert Harper (Carnegie Mellon), Xavier Leroy (INRIA), Conor  
McBride (Strathclyde), Greg Morrisett (Harvard), Frank Pfenning  
(Carnegie Mellon), Benjamin Pierce (Penn), and Andrew Tolmach  
(Portland State).

Please see  
for complete information about this year's summer school.  Please note  
that the registration deadline is MARCH 22, 2010.

We look forward to a great program!

Zena Ariola
Pierre-Louis Curien
Robert Harper
Hugo Herbelin

Attachment (smime.p7s): application/pkcs7-signature, 5285 bytes
Yves Bertot | 1 Mar 09:41 2010

[TYPES/announce] CFP: Call for papers, Coq Workshop (Edinburgh, July 9)

[ The Types Forum (announcements only), ]

lease help disseminate this call for papers

Two changes in the call for papers:

1/ papers describing experiments in other type theory-based proof 
assistants are explicitly invited to this workshop,

2/ EPTCS ( has agreed to host the proceedings.

Call for papers

The Coq workshop will bring together Coq users, developers and 
contributors. The workshop will be organized from submitted papers, 
invited talks and a plenary discussion on the evolution and design of 
Coq. Topics for submitting a paper include:

   * Experiments with type-theoretic proof assistants
   * Language or tactics features
   * Theory and implementation of the Calculus of Inductive Constructions
   * Applications and experience in education and industry
   * Tools, platforms built on Coq
   * Plugins, libraries for Coq
   * Interfacing with Coq
   * Formalization tricks and Coq pearls

Authors should submit their paper through EasyChair at the following link:

(Continue reading)

German Vidal | 1 Mar 20:41 2010

[TYPES/announce] CFP CICLOPS-WLPE 2010 at FLoC (Edinburgh, 15 July)

[ The Types Forum (announcements only), ]

                             Call For Papers

                            CICLOPS-WLPE 2010

                            Joint Workshop on
      Implementation of Constraint Logic Programming Systems
          Logic-based Methods in Programming Environments

                          Edinburgh, Scotland, U.K.
                             July 15, 2010

                         Satellite event of the
   26th International Conference on Logic Programming (ICLP 2010)


Important Dates:

Paper Submission:          March 31, 2010
Notification of Authors:   April 29, 2010
Camera-ready:              May 17, 2010 (tentative)
Workshop:                  July 15, 2010

(Continue reading)

Temur Kutsia | 1 Mar 22:53 2010

[TYPES/announce] 2nd CfP: PPDP'10

[ The Types Forum (announcements only), ]

                          Call for Papers
                             PPDP 2010
                12th International ACM SIGPLAN Symposium on
          Principles and Practice of Declarative Programming
                  Hagenberg, Austria, 26-28 July 2010
                     (co-located with LOPSTR 2010)


PPDP 2010 aims to bring together researchers from the declarative
programming communities, including those working in the logic,
constraint and functional programming paradigms, but also embracing a
variety of other paradigms such as visual programming, executable
specification languages, database languages, AI languages and
knowledge representation languages used, for example, in the semantic
web. The goal is to stimulate research in the use of logical
formalisms and methods for specifying, performing, and analysing
computations, including mechanisms for mobility, modularity,
concurrency, object-orientation, security, and static analysis. Papers
related to the use of declarative paradigms and tools in industry and
education are especially solicited.

The conference will take place in July 2010 in the Castle of
Hagenberg, Austria, colocated with the 20th International Symposium on
Logic-Based Program Synthesis and Transformation (LOPSTR 2010),
organised by the Research Institute for Symbolic Computation (RISC) of
(Continue reading)

Betti Venneri | 2 Mar 10:02 2010

[TYPES/announce] ITRS 2010 - 2nd CFP

[ The Types Forum (announcements only), ]

                          2nd CALL FOR PAPERS

                       Deadline: March 31, 2010

                             **ITRS 2010**

         Fifth Workshop on  Intersection Types and Related Systems
             (A FLoC workshop affiliated with LICS 2010)
                   July 9, 2010, Edinburgh, UK
Intersection types were introduced near the end of the 1970s to overcome
the limitations of Curry's type assignment system and to provide a
characterization of the strongly normalizing terms of the Lambda Calculus.
They have been one of the first examples of behavioural type theory:
namely, they provide an abstract specification of computational
properties, by expressing a finer and more precise input/output relation
than  standard, commonly used, type systems can do.

Although intersection types were initially intended for use in analysing
and/or synthesizing lambda models as well as in analysing normalization
properties, over the last twenty years the scope of the research on
intersection types and related systems has broadened in many directions.
Restricted (and more manageable) forms have been investigated, such as
refinement types. Type systems based on intersection type theory have
been extensively studied for practical purposes, such as program
(Continue reading)

Steve Kremer | 2 Mar 13:48 2010

[TYPES/announce] SecReT 2010

[ The Types Forum (announcements only), ]

5th International Workshop on Security and Rewriting Techniques
			(SecReT 2010)
		Valencia (Spain), June 18-20.

Aims and Scope:

We need to increase our confidence in security related applications.
Formal verification is one of the most important methods of achieving
this goal, and term rewriting has already played an important part. In
particular, since the beginning of formal verification of security
protocols, term rewriting has played a central role, both as a
computation model and as a deduction strategy. Because of this, we
believe that it can play an important role in solving other
security-related formal verification problems as well. That is why it
is important to bring together experts in term rewriting, constraint
solving, equational reasoning on the one side and experts in security
on the other side. This is precisely the aim of this workshop.

A possible (non exhaustive) list of topics include application of
rewriting or constraint solving to authentication, encryption, access
control and authorization, protocol verification, specification and
analysis of policies, intrusion detection, integrity of information,
control of information leakage, control of distributed and mobile
code, etc.

Submission instructions:

(Continue reading)


[TYPES/announce] Call for Participation NFM 2010

[ The Types Forum (announcements only), ]

CALL FOR PARTICIPATION: 2nd NASA Formal Methods Symposium

The NASA Formal Methods community invites you to attend the

Second NASA Formal Methods Symposium (NFM 2010)

April 13-15, 2010
Washington D.C.

Theme of Conference
The NASA Formal Methods Symposium is a forum for theoreticians and
practitioners from academia and industry, with the goals of identifying
challenges and providing solutions to achieving assurance in safety-critical
systems. The focus of the symposium will be on formal techniques, their
theory, current capabilities, and limitations, as well as their application
to aerospace, robotics, and other safety-critical systems.

Invited Speakers
Nikolaj Bjorner, Microsoft
Guillaume Brat, NASA
John Harrison,  Intel
(Continue reading)

Matt Kaufmann | 2 Mar 17:42 2010

[TYPES/announce] Result of Call for Votes on bids to host ITP-2011

[ The Types Forum (announcements only), ]

Hello --

Voting has closed for the Call for Votes on bids to host ITP-2011, as
announced on Feb. 18 (see  The
result was computed using VoteEngine 0.99, downloaded from, and the output is shown below.  (I also
wrote my own little program to compute each round and checked that its
results completely agreed with those of VoteEngine.  I also checked
and fixed spelling typos.)

Congratulations to the team from The Netherlands on its winning bid!
And thank you to all of those who submitted bids, which we found to be
very impressive.

In the output below, we have of course:

C = China
D = Denmark
N = Netherlands
S = Spain


VOTES   61
(Continue reading)

Vladimiro Sassone | 3 Mar 07:20 2010

[TYPES/announce] deadline extension: IFIP TCS 2010

[ The Types Forum (announcements only), ]

Dear colleagues,  

This is to announce a deadline extension for submissions of papers to

	6th IFIP International Conference on Theoretical Computer Science

a part of the 

	IFIP World Computer Congress 2010
	Brisbane, Australia
	20-23 September 2010

Please consider submitting your work by the new deadline:
	Deadline for abstracts: Mar 12th 
	Deadline for papers: 	  Mar 15th.

The CfP is available at 

(please ignore the old submission date on that page).

Submission at 

With best regards,
(Continue reading)

Matthew Fluet | 3 Mar 16:08 2010

[TYPES/announce] Workshop on ML 2010 - Call for Content

[ The Types Forum (announcements only), ]

                  The 2010 ACM SIGPLAN Workshop on ML
                   Baltimore, Maryland, United States
                       Sunday, September 26, 2010
                       co-located with ICFP 2010

                            Call for Content

ML is a family of programming languages that includes dialects known
as Standard ML, Objective Caml, and F#. The development of these
languages has inspired a large amount of computer science research,
both practical and theoretical. This workshop aims to provide a forum
to encourage discussion and research on ML and related technology
(higher-order, typed, or strict languages).

The format of the 2010 Workshop on ML will be different than that of
recent years, returning to a more informal model: a workshop with
presentations selected from submitted abstracts but without published
proceedings. We hope that this format will encourage the presentation
of more exciting (if unpolished) research and deliver a more lively
workshop atmosphere.

Important Dates

(Continue reading)