[TYPES] CFP: CLASE at ETAPS deadline extension

[Iman Hafiz Poernomo]

Dear colleague,

I draw your attention to the following workshop at ETAPS 2005 in Edinburgh:
Constructive Logic for Automated Software Engineering
http://www.dcs.kcl.ac.uk/events/clase/
Please find the CFP attached. The title of the workshop sounds rather
specific, but we are open to any kind of type theoretic/logic-based
theories/methodologies/tools that could help make software construction more
reliable. 

Due to several requests, it has been decided to move to paper submission
deadline for CLASE to February 11th. 

This also gives you a chance to submit something! Long papers and abstracts
can be submitted. After the workshop, papers will be published in a volume
of Elsevier's ENTCS (abstracts can be extended for publication in this
also). Publication of best papers is also expected to be given in a special
issue of a major logic journal -- so it is well worth putting something in. 

The workshop promises to be an interesting one and we are lucky to have Alan
Bundy as invited speaker -- so please forward this CFP to any colleagues who
might be interested. 

Best wishes and happy New Year,


Iman

--------------
Iman Poernomo
Lecturer
Department of Computer Science
King's College London
iman at dcs.kcl.ac.uk


-------------- next part --------------
CALL FOR PAPERS

 Constructive Logic for
  Automated Software Engineering (CLASE 2005)

 http://www.dcs.kcl.ac.uk/events/clase/

 Satellite event of ETAPS 2005,
  Edinburgh, 3rd April 2005

Scope

This workshop will provide an avenue for work that extends
traditional methods that derive from constructive logic for
synthesizing complex software. After more than 30 years of research,
program synthesis using constructive logic constitutes a mature
field with an established theory and set of best practices. Recent
years have seen an interest in providing analogous results to other
logical systems and programming languages. This workshop will bring
together researchers and practitioners to share ideas on the
foundations, techniques, tools, and applications of constructive
logic and its methods to automated software engineering technology.

This workshop will provide an avenue for work that extends
traditional methods that derive from constructive logic for
synthesizing complex software.

Software engineering is concerned with processes and techniques for
analysis, design, implementation, testing, and maintenance of
software systems. Automated software engineering is concerned with
computational techniques to automate these tasks (at least
partially) in order to aid reliability, trustworthiness and
productivity of code and of the engineering process itself.

The application of constructive logic to small-scale functional
program synthesis is well known. One pervasive idea is that the
constructive content of a proof of a formula can be transformed into
a functional program that satisfies the formula when the latter is
regarded as a specification. Such work, based upon the Curry-Howard
isomorphism and higher-order type theory, constitutes the area
referred to as the proofs-as-programs paradigm.

Other areas that are susceptible to the use of constructive logic
include

? Type theory in general,

? Proof planning,

? Constructive tableaux,

? Labelled Deductive systems and hybrid logics in general,

? Deductive logic programming.

The advantage of proofs-as-programs techniques is that the task of
programming a function is reduced to reasoning with domain
knowledge, transforming constructive proofs to a commonly used
functional programming language that can encode a simply typed
lambda calculus, such as SML, Scheme or Haskell.

After more than 30 years of research, proofs-as-programs constitutes
a mature field with an established theory and set of best practices.
Recent years have seen an interest in providing analogous results to
other logical systems and programming languages.

This workshop will bring together researchers and practitioners to
share ideas on the foundations, techniques, tools, and applications
of constructive logic and its methods to automated software
engineering technology.

Topics

We encourage submissions on techniques that involve constructive
reasoning, analysis and synthesis for complex software engineering.
Examples include:

? proofs-as-programs adapted to logics other than intuitionistic logic
(e.g., linear logic, Hennesy-Milner specification systems, modal
logic, temporal logic)

? proofs-as-programs for program synthesis in complex programming
paradigms (e.g., distributed, object-oriented, component-based or
embedded systems),

? constructive logics for semantic foundations of modelling and
requirements languages,

? integration of ideas from constructive logic into software
engineering process design,

? evaluative case studies of constructive methods for large scale
system development,

? industrial strength, constructive synthesis, system implementations.

Guest Speaker

Alan Bundy, School of Informatics, University of Edinburgh, UK.

Dates

Submission deadline: 11th February 2005

Notification of acceptance/rejection: 21st February 2005

Final version: 28th February 2005

Submissions

There are two kinds of submission accepted: short (no longer than 2
pages) and long (no longer than 10 pages) papers. Submissions should
include author's full name(s), affiliation(s) and address(es),
phone- and fax-number(s) and email address(es). Papers in PS or
PDF-format should be emailed to the address iman 'at symbol' dcs.kcl.ac.uk,
with the subject heading "CLASE submission". All valid submissions will be
reviewed by at least two members of the program committee.

Publication Final versions of accepted full papers are to
be published in a special issue of the Electronic Notes in Computer
Science (ENTCS).  Authors of accepted short papers will have the
opportunity to submit expanded versions of their papers for a second
round of review for publication in the special issue.

Organizing Committee

Stuart F. Allen, sfa 'at symbol' cs.cornell.edu, Department of
Computer Science, Cornell University, USA

John Crossley, John.Crossley 'at symbol'  infotech.monash.edu.au,
School of Computer Science and Software Engineering, Monash
University, Australia

Kung-Kiu Lau, kung-kiu 'at symbol' cs.man.ac.uk, Department of
Computer Science, University of Manchester, UK

Iman Poernomo, iman 'at symbol' dcs.kcl.ac.uk, Department of Computer
Science, King's College London, UK


Program Committee

Stuart F. Allen, Cornell University, USA

Ulrich Berger, University of Wales Swansea, UK

James Caldwell, University of Wyoming, USA

Karl Crary, Carnegie Mellon University, USA

John Crossley, Monash University, Australia

Ewen Denney, University of Edinburgh, UK

Raj Gore, Australian National University, Australia

Douglas J. Howe, Carleton University, Canada

Kung-Kiu Lau, University of Manchester, UK

Mihhail Matskin, Royal Institute of Technology, Sweden

Mario Ornaghi, Universita' degli studi di Milano, Italy

Christine Paulin-Mohring, Université Paris Sud, France

Iman Poernomo, Monash University, Australia

Anton Setzer, University of Wales Swansea, UK

Alex Simpson, University of Edinburgh, UK

Martin Wirsing, Ludwig-Maximilians Universität, Germany