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/categorical/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@dcs.kcl.ac.uk 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=E9 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=E4t, Germany ------=_NextPart_000_073A_01C4F7DE.E8604480-- 12-Jan-2005 12:21:18 -0400,4350;000000000000-00000000