headers
Johan Jeuring | 3 Sep 1999 18:15
Picon

Workshop on Generic Programming 2000, call for papers


               Workshop on Generic Programming

     http://www.cs.uu.nl/~johanj/wgp2000/wgp2000cfp.html

                         6th July 2000

                   Ponte de Lima, Portugal

                        Call for papers

Generic programming is about making programs more adaptable by making them
more general. Generic programs often embody non-traditional kinds of
polymorphism; ordinary programs are obtained from them by suitably
instantiating their parameters. In contrast with normal programs, the
parameters of a generic programs are often quite rich in structure. For
example they may be other programs, types or type constructors, kinds, or
even programming paradigms. 

This workshop follows on the 5th Mathematics of Program Construction
conference. 

This is the second workshop on generic programming, the first workshop on
generic programming (proceedings) was held on Marstrand, Sweden, in 1998. 

                         Submission

Papers (preferably short, no more than 15 pages) should be submitted in
Postscript format by e-mail to reach Johan Jeuring by March 20, 2000.
Accepted papers will be published in the proceedings of the workshop, which
(Continue reading)

Permalink | Reply | 0 comments |
headers
Gert Smolka | 6 Sep 1999 14:24
Picon

ESOP 2000: Call for Papers

First Call for Papers:

			    ESOP 2000
		  European Symposium on Programming
		  March 27-31, 2000, Berlin, Germany
		  http://www.ps.uni-sb.de/~esop2000
                  Submission deadline:  Oct 18, 1999

Program Chair:  Gert Smolka, Uni Saarbruecken, Germany

Invited Speaker: Martin Odersky, EPF Lausanne, Switzerland

PC:     Gerard Boudol,  INRIA, Sophia-Antipolis, France
        Sophia Drossopoulou,  Imperial College, London, UK
        Matthias Felleisen,  Rice University, Houston, US
        Michael Franz,  UC Irvine, US
        Manuel Hermenegildo,  TU Madrid, Spain
        Xavier Leroy,  INRIA Rocquencourt, France
        Alan Mycroft,  Cambridge University, UK
        Martin Odersky,  EPF Lausanne, Switzerland
        Andreas Podelski,  MPI, Saarbruecken, Germany
        Gert Smolka, UdS,  Saarbruecken, Germany
        Peter Thiemann,  Uni Freiburg, Germany
        Mads Tofte,  Uni Copenhagen, Denmark
        Pascal van Hentenryck,  Uni Louvain, Belgium

ESOP is an annual conference devoted to the design,
specification and analysis of programming languages and
programming systems. Both practical and theoretical papers
are welcome. Possible topics include: Programming paradigms
(Continue reading)

Permalink | Reply | 0 comments |
headers
David Naumann | 10 Sep 1999 00:44
Picon

research positions available

Stevens Institute of Technology, just across the Hudson river from 
New York City

A number of other research assistantships for PhD students, and
post-doc positions, are available in the department of computer
science.  The research interests of the group include mobile code and
security, software design and validation, program analysis and
verification, type systems, networks and wireless, computer vision and
data mining.

This announcement concerns the research of David Naumann:

A Research Assistant (PhD student) is sought for a collaborative
project between faculty at Stevens, the University of Illinois, and
the Federal University of Pernambuco, Brazil.  The topic is behavioral
refinement of Java-like programs. We are developing two semantic
models of programs and their specifications, and using those models to
validate laws of refinement.  Some laws express design steps such as
re-structuring a class hierarchy.  Other laws are used to reduce
programs to a normal form corresponding to machine code, as a basis
for correct compilation.  (Position funded by NSF.)

A Research Assistant or post-doc is sought for a collaborative project
on applications of model-checking in program analysis for security and
other properties such as dynamic typing.  (Position funded by Stevens
and a corporate partner.)

Both positions are available now but need not be filled immediately.
Candidates are expected to have a background in computer science with
a strong interest in research.  Candidates are asked to send a vita
(Continue reading)

Permalink | Reply | 0 comments |
headers
Dave Stringer-Calvert | 10 Sep 1999 06:51
Favicon

Announcing PVS Version 2.3


We are pleased to announce the release of PVS 2.3.

PVS is a widely used theorem proving tool.  It is in roughly the same
class of systems as HOL, Nuprl, Isabelle, Coq, LEGO, etc.  It is a theorem
prover for a strongly typed higher-order logic based on Church's theory of
types.  It has a modern and novel type system based on predicate subtypes
and dependent types so that typechecking involves theorem proving.  A
fragment of the PVS language can also be used as an (extremely fast)
strongly typed functional language that exploits a number of type-based
optimizations.

Details are available at the PVS web site http://pvs.csl.sri.com

We hope you find PVS useful and fun,

The PVS Team
pvs-bugs@...
Permalink | Reply | 0 comments |
headers
Carolyn Talcott | 15 Sep 1999 21:53
Picon

FMOODS 2000 Preliminary Call for Papers


                       Preliminary Call for Papers

                     Fourth IFIP International conference 
				     on
	  Formal Methods for Open Object-based Distributed Systems

				FMOODS'2000

                Stanford California, USA, 4th-6th September, 2000

  ------------------------------------------------------------------------

Objectives

Object-based Distributed Computing is being established as the most
pertinent basis for the support of large, heterogeneous computing and
telecommunications systems. Indeed, several important international
organisations, such as ITU, ISO, OMG, TINA-C, etc. are defining similar
distributed object-based frameworks as a foundation for open distributed
computing.

The advent of Open Object-based Distributed Systems - OODS - brings new
challenges and opportunities for the use and development of formal methods.
New architectures and system models are emerging (e.g., the enterprise,
information, computational and engineering viewpoints of the ITU-T/ISO/IEC
ODP Reference Model) which require formal notational support. Usual design
issues such as specification, verification, refinement, and testing need to
take into account new dimensions introduced by distribution and openness,
such as quality of service and dependability constraints, dynamic binding
(Continue reading)

Permalink | Reply | 0 comments |
headers
Carolyn Talcott | 16 Sep 1999 06:45
Picon

FMOODS 2000 CFP correction


[[many apologies for duplication both in mailing list and mailing.
  In the previous announcement the conference dates were wrong.
  The correct dates are Wed-Fri 6th-8th September 2000]]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

                       Preliminary Call for Papers

                     Fourth IFIP International conference 
				     on
	  Formal Methods for Open Object-based Distributed Systems

				FMOODS'2000

                Stanford California, USA, 6th-8th September, 2000

  ------------------------------------------------------------------------

Objectives

Object-based Distributed Computing is being established as the most
pertinent basis for the support of large, heterogeneous computing and
telecommunications systems. Indeed, several important international
organisations, such as ITU, ISO, OMG, TINA-C, etc. are defining similar
distributed object-based frameworks as a foundation for open distributed
computing.

The advent of Open Object-based Distributed Systems - OODS - brings new
challenges and opportunities for the use and development of formal methods.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Georges Mounier | 20 Sep 1999 10:48
Picon
Favicon

New paper: an intuitionistic lambda-calculus with exceptions


I am pleased to announce my PhD thesis, (Universite de Savoie, France,
 19 fevrier 19999) available (in french) at the author : 
 mounier@...

Regards,
     Georges Mounier

------------------------------------------------------------------------

AN INTUITIONISTIC LAMBDA-CALCULUS WITH EXCEPTIONS
Georges Mounier                                  

Abstract:

The thesis describes a typed lambda-calculus extended with a mechanism 
for exceptions.

Typed lambda-calculus is a good theoretical model for the functional
 aspects of programming languages, but not for exceptions. 
We first  examine typed lambda-calculi recently proposed to give a
 logical interpretation of control mechanisms, and we show that no one
 of them is a satisfying description of exceptions - as they are
 implemented, for example, in the Caml language.
Then, we describe a new typed lambda-calculus, named Ex2, which 
allows to declare, raise and handle exceptions.

The main properties of Ex2 are proved :
confluence of the calculus, strong normalization of typed terms, subject
reduction for a parallel notion of reduction and preservation of data
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jerzy Tiuryn | 20 Sep 1999 19:14
Picon
Picon

FOSSACS 2000, Call for Papers


                         CALL FOR PAPERS

                          FOSSACS 2000
     Foundations of Software Science and Computation Structures
                 March 27-31, 2000, Berlin, Germany
	         http://fossacs.mimuw.edu.pl
	        Submision deadline: October 18, 1999

                          A member conference of 
    the European Joint Conferences on Theory and Practice of Software 
                          (ETAPS 2000)

Conference decsription:

FOSSACS seeks papers which offer progress in foundational research
with a clear significance for software science. A central issue is
theories and methods which support the specification, transformation,
verification, and analysis of programs and software systems.

Topics covered are:

**    Computational and syntactic foundations of software science:
      computation processes over discrete and continuous data,
      techniques for their manipulation, and their algorithmic, 
      algebraic, and logical properties;

**   Transition systems, models of concurrency and reactive systems,
      and corresponding calculi, algebras, and logics;
(Continue reading)

Permalink | Reply | 0 comments |
headers
Marta Z Kwiatkowska | 23 Sep 1999 15:09
Picon
Picon
Favicon

FOSSACS'2000: Call for papers

                          CALL FOR PAPERS

                          FOSSACS 2000
     Foundations of Software Science and Computation Structures
                 March 27-31, 2000, Berlin, Germany
	         http://fossacs.mimuw.edu.pl
	        Submision deadline: October 18, 1999

                          A member conference of 
    the European Joint Conferences on Theory and Practice of Software 
                          (ETAPS 2000)

Conference decsription:

FOSSACS seeks papers which offer progress in foundational research
with a clear significance for software science. A central issue is
theories and methods which support the specification, transformation,
verification, and analysis of programs and software systems.

Topics covered are:

**    Computational and syntactic foundations of software science:
      computation processes over discrete and continuous data,
      techniques for their manipulation, and their algorithmic, 
      algebraic, and logical properties;

**   Transition systems, models of concurrency and reactive systems,
      and corresponding calculi, algebras, and logics;

**   Type theory, domain theory, and their connections to semantics
(Continue reading)

Permalink | Reply | 0 comments |
headers
Isabelle Attali | 24 Sep 1999 13:43
Picon
Picon
Favicon

Job Opportunity at INRIA Sophia Antipolis


[The position involves substantial work with type-theory based
proof-development systems and may therefore be of interest to
the TYPES readers.]

RESEARCH & DEVELOPMENT POSITION IN FORMAL METHODS
FOR SMARTCARD SECURITY

INRIA Sophia-Antipolis opens one 2-year position in the Oasis team.
The position is connected to Formavie, a joint project between Bull,
Schlumberger and INRIA, and  partially supported by the French Ministry
of Economy, Finances and Industry.

The goal of Formavie is to provide secure embbeded software for the
success
of electronic commerce. The role of INRIA in Formavie is to provide
formal tools
and methodology to ensure security for embedded software and in
particular smartcards
and terminals. The main task involved is the design and development of a
toolset for  the
formalization, analyzis, transformation and visualization  of models of
embedded systems
(virtual machines) and security policies for those systems.

The position offers opportunities for innovative and collaborative
research in the area of
formal verification as well as for developing applications to be used in
an industrial context,
with a challenging goal: achieving for the embedded systems  a
(Continue reading)

Permalink | Reply | 0 comments |

Gmane