Scope Workshop program now available. Click here to register for ETAPS and/or CLASE. 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: Constructing Induction Rules for Deductive Synthesis Proofs.

Workshop program

Time
8:30 - 9:00	Registration
9:00 - 9:05	Welcome and introduction (the organizers)
9:05 - 10:00	1st Session. Invited Talk, Alan Bundy: Constructing Induction Rules for Deductive Synthesis Proofs, Alan Bundy, Jeremy Gow Jacques Fleuriot and Lucas Dixon
10:00 - 10:30	2nd Session. ESBC: an application for computing stabilization bounds, Alessandro Avellone, Mauro Ferrari, Camillo Fiorentini, Guido Fiorino, Ugo Moscato
10:30 - 11:00	Coffee Break
11:00 - 12:30	3rd Session. A Constructive Modeling Language for Object Oriented Information Systems, Mario Ornaghi, Marco Benini, Mauro Ferrari, Camillo Fiorentini, Alberto Momigliano Automatic Complexity Analysis for Programs Extracted from Coq Proof, Jean-Pierre Jouannaud and Weiwen Xu Gallimaufry: An Automated Framework for Proving Type-Safety, Anne Mulhern
12:30 - 14:00	Lunch
14:00 - 15:30	4th Session Specifications via Realizability, Andrej Bauer and Christopher A. Stone. Constructive MDA, Iman Poernomo (organizer's talk -- not included in proceedings) Building new constructive logical systems, John Crossley (organizer's talk -- not included in proceedings) Group discussion: applied constructive methods.
Evening	ETAPS workshops dinner

Dates

Workshop: 9th April 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 workshop email 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

John Crossley, Monash University, Australia

Ewen Denney, NASA Ames Research Center, USA

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