[Caml-list] AI4FM 2013 : First Call For Papers (ITP 2013 workshop)

Apologies for multiple copies

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

  AI4FM 2013 - the 4th International Workshop on

    the use of AI in Formal Methods

      

       http://www.ai4fm.org/ai4fm-2013/

    Rennes, France, 22nd July, 2013

     In association with ITP 2013

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

          --- First Call for Papers ---

General

-------

This workshop will bring together researchers from formal methods and AI; it will address the 

issue of how AI can be used to support the formal software development process, including modelling 

and proof. Previous AI4FM workshops have included a mix of industrial and academic participants 

and we anticipate attracting a similarly diverse audience. 

Industrial use of formal methods is certainly increasing but, in order to make it more mainstream, 

the cost of applying formal methods, in terms of mathematical skill level and development time, 

must be reduced — we believe that AI can help with these issues. 

Rigorous software development using formal methods allows the construction of an accurate characterisation 

of a problem domain that is firmly based on mathematics; by applying standard mathematical analyses, these 

methods can be used to prove that systems satisfy formal specifications. A recent ACM computing survey paper 

describes over sixty industrial projects and discusses the effect formal methods have on time, cost and quality. 

It shows that with tools backed by mature theory, formal methods are becoming cost effective and their use is 

easier to justify, not as an academic exercise or legal requirement, but as part of a business case. Furthermore, 

the use of such formal methods is no longer confined to safety critical systems: the list of industrial partners 

in the EU-funded DEPLOY project is one indication of this broader use. Most methods tend to fit a ``posit-and-prove'' 

paradigm where the user posits a development step (expressed in terms of specifications of yet-to-be-realised components) 

that has to be justified by proofs. The associated properties that must be verified are often called proof obligations (POs) 

or verification conditions. In most cases, such proofs require mechanical support by theorem provers. 

One can distinguish between automatic and interactive provers, where the latter are generally more expressive but require 

user interaction. AI has had a large impact on the development of provers. In fact, some of the first AI applications were 

in theorem proving and all theorem provers now contain heuristics to reduce the search space that can be attributed to AI. 

Nevertheless, theorem proving research and (pure) AI research have diverged and theorem proving is barely considered 

to be AI-related anymore. 

Scope

-----

We encourage submissions presenting work in progress, tools under

development, and PhD projects, in order that the

workshop can become a forum for active dialogue between the groups

involved in  theorem provers, formal methods and artificial intelligence.

Particular areas of interest include, but are not limited to:

 * The use of machine learning to support interactive theorem proving;

 * The use of machine learning to enhance automated theorem proving;

 * The development of search heuristics;

 * The us of AI for term synthesis, invariant generation, lemma discovery and concept invention;

 * The use of AI for counter-example generation;

 * The use of AI to support and guide the formal modelling process;

 * The role of AI planning for formal systems developments, from requirements to the end product (including software and hardware);

 * The interplay between reasoning and modelling and the role of AI in this framework;

 * Ontologies in the formal engineering process.

Submission

----------

The main aim for the workshop is discussion, thus submissions 

do not need to be original. Extended versions of submissions

may have been published previously, or submitted concurrently with 

or after AI4FM 2013 to another workshop, conference or a journal.

Submission is by email to:

  ai4fm2013@ai4fm.org

Please submit an abstract up to 3 pages in a PDF format. The extended

abstracts will be handed out to all participants, and will be made into

a technical report prior to the workshop. 

Acceptance for presentation at the workshop will be made by the

organisers based on relevance to the workshop.

Important Dates

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

Submission deadline: April 20, 2013

Notification of acceptance: May 01, 2013

Final version due: May 15, 2013

Workshop: July 22nd, 2013

Organisers

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

* Leo Freitas (Newcastle University, UK)

* Gudmund Grov (Heriot-Watt University, UK)

* Ewen Maclean (University of Edinburgh, UK)

Contact Details

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

If you have any queries, please email the organisers at the following email address:

  ai4fm2013@ai4fm.org

[Caml-list] Second Call For Papers: Conf. Intelligent Computer Mathematics (CICM 2013), July 8-12, 2013, Bath, UK

CICM 2013 - Conferences on Intelligent Computer Mathematics
July 8-12, 2013 at University of Bath, Bath, UK

http://www.cicm-conference.org/2013/cicm.php

2nd Call for Papers

----------------------------------------------------------------------
* Invited Talks by
Patrick Ion (Mathematical Reviews, American Mathematical
Society, USA)
Assia Mahboubi (École Polytechnique and INRIA/Microsoft
Research Joint Centre, France)
Ursula Martin (Queen Mary, University of London, UK)

* Co-Located Workshops:
- MathUI'13: Mathematical User Interfaces
- OpenMath Workshop 2013
- PLMMS'13: Programming Languages for Mechanized Mathematics Systems
- THedu'13: TP Components for Educational Software
----------------------------------------------------------------------

As computers and communications technology advance, greater
opportunities arise for intelligent mathematical computation. While
computer algebra, automated deduction, mathematical publishing and
novel user interfaces individually have long and successful histories,
we are now seeing increasing opportunities for synergy among these
areas. The Conferences on Intelligent Computer Mathematics offers a
venue for discussing these areas and their synergy.

The conference will take place at the University of Bath
(www.bath.ac.uk), with James Davenport as the local organiser. It
consists of four tracks:

Calculemus
Chair: Wolfgang Windsteiger
Digital Mathematical Libraries (DML)
Chair: Petr Sojka
Mathematical Knowledge Management (MKM)
Chair: David Aspinall
Systems and Projects
Chair: Christoph Lange

As in previous years, there will be a Doctoral Programme for
presentations by Doctoral students.

The overall programme will be organised by the General Program Chair
Jacques Carette.

----------------------------------------------------------------------
Important dates
----------------------------------------------------------------------

Abstract submission: 1 March 2013
Submission deadline: 8 March 2013
Reviews sent to authors: 5 April 2013
Rebuttals due: 8 April 2013
Notification of acceptance: 14 April 2013
Camera ready copies due: 26 April 2013
Conference: 8-12 July 2013

----------------------------------------------------------------------
Tracks
----------------------------------------------------------------------

==========
Calculemus
==========

Calculemus 2013 invites the submission of original research
contributions to be considered for publication and presentation at the
conference. Calculemus is a series of conferences dedicated to the
integration of computer algebra systems (CAS) and systems for
mechanised reasoning like interactive proof assistants (PA) or
automated theorem provers (ATP). Currently, symbolic computation is
divided into several (more or less) independent branches: traditional
ones (e.g., computer algebra and mechanised reasoning) as well as
newly emerging ones (on user interfaces, knowledge management, theory
exploration, etc.) The main concern of the Calculemus community is to
bring these developments together in order to facilitate the theory,
design, and implementation of integrated mathematical assistant
systems that will be used routinely by mathematicians, computer
scientists and all others who need computer-supported mathematics in
their every day business.

All topics in the intersection of computer algebra systems and
automated reasoning systems are of interest for Calculemus. These
include but are not limited to:

* Automated theorem proving in computer algebra systems.
* Computer algebra in theorem proving systems.
* Adding reasoning capabilities to computer algebra systems.
* Adding computational capabilities to theorem proving systems.
* Theory, design and implementation of interdisciplinary systems for
computer mathematics.
* Case studies and applications that involve a mix of computation and
reasoning.
* Case studies in formalization of mathematical theories.
* Representation of mathematics in computer algebra systems.
* Theory exploration techniques.
* Combining methods of symbolic computation and formal deduction.
* Input languages, programming languages, types and constraint languages,
and modeling languages for mathematical assistant systems.
* Homotopy type theory.
* Infrastructure for mathematical services.

===
DML
===

Mathematicians dream of a digital archive containing all peer-reviewed
mathematical literature ever published, properly linked, validated and
verified. It is estimated that the entire corpus of mathematical
knowledge published over the centuries does not exceed 100,000,000
pages, an amount easily manageable by current information
technologies.

Track objective is to provide a forum for development of math-aware
technologies, standards, algorithms and formats towards fulfillment of
the dream of global digital mathematical library (DML). Computer
scientists (D) and librarians of digital age (L) are especially
welcome to join mathematicians (M) and discuss many aspects of DML
preparation.

Track topics are all topics of mathematical knowledge management and
digital libraries applicable in the context of DML building --
processing of math knowledge expressed in scientific papers in natural
languages, namely:

* Math-aware text mining (math mining) and MSC classification
* Math-aware representations of mathematical knowledge
* Math-aware computational linguistics and corpora
* Math-aware tools for [meta]data and fulltext processing
* Math-aware OCR and document analysis
* Math-aware information retrieval
* Math-aware indexing and search
* Authoring languages and tools
* MathML, OpenMath, TeX and other mathematical content standards
* Web interfaces for DML content
* Mathematics on the web, math crawling and indexing
* Math-aware document processing workflows
* Archives of written mathematics
* DML management, business models
* DML rights handling, funding, sustainability
* DML content acquisition, validation and curation

===
MKM
===

Mathematical Knowledge Management is an interdisciplinary field of
research in the intersection of mathematics, computer science, library
science, and scientific publishing. The objective of MKM is to develop
new and better ways of managing sophisticated mathematical knowledge,
based on innovative technology of computer science, the Internet, and
intelligent knowledge processing. MKM is expected to serve
mathematicians, scientists, and engineers who produce and use
mathematical knowledge; educators and students who teach and learn
mathematics; publishers who offer mathematical textbooks and
disseminate new mathematical results; and librarians and
mathematicians who catalog and organize mathematical knowledge.

The conference is concerned with all aspects of mathematical knowledge
management. A non-exclusive list of important topics includes:

* Representations of mathematical knowledge
* Authoring languages and tools
* Repositories of formalized mathematics
* Deduction systems
* Mathematical digital libraries
* Diagrammatic representations
* Mathematical OCR
* Mathematical search and retrieval
* Math assistants, tutoring and assessment systems
* MathML, OpenMath, and other mathematical content standards
* Web presentation of mathematics
* Data mining, discovery, theory exploration
* Computer algebra systems
* Collaboration tools for mathematics
* Challenges and solutions for mathematical workflows

====================
Systems and Projects
====================

The Systems and Projects track of the Conferences on Intelligent
Computer Mathematics is a forum for presenting available systems and
new and ongoing projects in all areas and topics related to the CICM
conferences:

* Deduction and Computer Algebra (Calculemus)
* Digital Mathematical Libraries (DML)
* Mathematical Knowledge Management (MKM)
* Artificial Intelligence and Symbolic Computation (AISC)

The track aims to provide an overview of the latest developments and
trends within the CICM community as well as to exchange ideas between
developers and introduce systems to an audience of potential users.

----------------------------------------------------------------------
Submission Instructions
----------------------------------------------------------------------

Submissions to the research tracks must not exceed 15 pages and will
be reviewed and evaluated with respect to relevance, clarity, quality,
originality, and impact. Shorter papers, e.g., for system
descriptions, are welcome. Authors will have an opportunity to respond
to their papers' reviews before the programme committee makes a
decision.

System descriptions and projects descriptions should be 2-4 pages and
should present
* newly developed systems,
* systems that have not previously been presented to the CICM community,
or
* significant updates to existing systems.
Systems must be available for download.

Project presentations should describe
* projects that are new or about to start,
* ongoing projects that have not yet been presented to the CICM community.
* significant new developments in ongoing previously presented projects.

Presentations of new projects should mention relevant previous work
and include a roadmap that outlines concrete steps. All submissions
should contain links to demos, downloadable systems, or project
websites.

Accepted conference submissions from all tracks is intended to be
published as a volume in the series Lecture Notes in Artificial
Intelligence (LNAI) by Springer. In addition to these formal
proceedings, authors are permitted and encouraged to publish the final
versions of their papers on arXiv.org.

Work-in-progress submissions are intended to provide a forum for the
presentation of original work that is not (yet) in a suitable form for
submission as a full or system description paper. This includes work
in progress and emerging trends. Their size is not limited, but we
recommend 5-10 pages.

The programme committee may offer authors of rejected formal
submissions to publish their contributions as work-in-progress papers
instead. Depending on the number of work-in-progress papers accepted,
they will be presented at the conference either as short talks or as
posters. The work-in-progress proceedings will be published as a
technical report, as well as online with CEUR-WS.org.

All papers should be prepared in LaTeX and formatted according to the
requirements of Springer's LNCS series (the corresponding style files
can be downloaded from
http://www.springer.de/comp/lncs/authors.html). By submitting a paper
the authors agree that if it is accepted at least one of the authors
will attend the conference to present it.

Electronic submission is done through easychair
http://www.easychair.org/conferences/?conf=cicm2013

----------------------------------------------------------------------
Programme Committee
----------------------------------------------------------------------

Akiko Aizawa, NII, The University of Tokyo, Japan
Jesse Alama, CENTRIA, FCT, Universidade Nova de Lisboa, Portugal
Rob Arthan, Queen Mary University of London, UK
Andrea Asperti, University of Bologna, Italy
David Aspinall, University of Edinburgh, UK
Jeremy Avigad, Carnegie Mellon University, US
Thierry Bouche, Université Joseph Fourier (Grenoble), France
Jacques Carette, McMaster University, Canada
John Charnley, Department of Computing, Imperial College London, UK
Janka Chlebíková, School of Computing, University of Portsmouth, UK
Simon Colton, Department of Computing, Imperial College, London, UK
Leo Freitas, Newcastle University, UK
Deyan Ginev, Jacobs University Bremen, Germany
Gudmund Grov, Heriot-Watt University, Edinburgh, UK
Thomas Hales, University of Pittsburgh, US
Yannis Haralambous, Télécom Bretagne, France
Jónathan Heras, University of Dundee, UK
Hoon Hong, North Carolina State University, US
Predrag Janičić, University of Belgrade, Serbia
Cezary Kaliszyk, University of Innsbruck, Austria
Manfred Kerber, University of Birmingham, UK
Adam Kilgarriff, Lexical Computing Ltd, UK
Andrea Kohlhase, Jacobs University Bremen, Germany
Michael Kohlhase, Jacobs University Bremen, Germany
Temur Kutsia, RISC Institute, JKU Linz, Austria
Christoph Lange, University of Birmingham, UK
Paul Libbrecht, Martin Luther University Halle-Wittenberg, Germany
Christoph Lüth, DFKI Bremen, Germany
Till Mossakowski, DFKI Bremen, Germany
Magnus O. Myreen, University of Cambridge, UK
Florian Rabe, Jacobs University Bremen, Germany
Jiří Rákosník, Institute of Mathematics, Academy of Sciences, Czech Republic
Carsten Schuermann, IT University of Copenhagen, Denmark
Petr Sojka, Masaryk University, Faculty of Informatics, Czech Republic
Hendrik Tews, TU Dresden, Germany
Frank Tompa, University of Waterloo, Canada
Josef Urban, Radboud University, Netherlands
Stephen Watt, University of Western Ontario, Canada
Makarius Wenzel, Université Paris-Sud 11, France
Wolfgang Windsteiger, RISC Institute, JKU Linz, Austria
Richard Zanibbi, Rochester Institute of Technology, US

--

Dr. Serge Autexier, serge.autexier@dfki.de, http://www.dfki.de/~serge/
Research Department Cyber-Physical Systems
MZH, Room 3120 Phone: +49 421 218 59834
Bibliothekstr.1, D-28359 Bremen Fax: +49 421 218 98 59834
----------------------------------------------------------------------
Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH
principal office, *not* the address for mail etc.!!!:
Trippstadter Str. 122, D-67663 Kaiserslautern
management board: Prof. Wolfgang Wahlster (chair), Dr. Walter Olthoff
supervisory board: Prof. Hans A. Aukes (chair)
Amtsgericht Kaiserslautern, HRB 2313
----------------------------------------------------------------------

--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] ICFP 2013: Call for papers

=====================================================================     18th ACM SIGPLAN International Conference on Functional Programming     ICFP 2013     Boston, MA, USA, 25-27 September 2013     http://www.icfpconference.org/icfp2013    =====================================================================    Important Dates  ~~~~~~~~~~~~~~~       Submissions due:  Thursday, 28 March 2013 23:59 UTC-11                                           (Pago Pago, American Samoa, time)     Author response:  Wednesday, 22 May 0:00 UTC-11                          Friday, 24 May 2013 23:59 UTC-11        Notification:  Friday, 7 June 2013      Final copy due:  Friday, 5 July 2013    Scope  ~~~~~    ICFP 2013 seeks original papers on the art and science of functional  programming.  Submissions are invited on all topics from principles to  practice, from foundations to features, and from abstraction to  application.  The scope includes all languages that encourage  functional programming, including both purely applicative and  imperative languages, as well as languages with objects, concurrency,  or parallelism.  Topics of interest include (but are not limited to):    * Language Design: concurrency and distribution; modules; components    and composition; metaprogramming; interoperability; type systems;    relations to imperative, object-oriented, or logic programming    * Implementation: abstract machines; virtual machines; interpretation;    compilation; compile-time and run-time optimization; memory    management; multi-threading; exploiting parallel hardware; interfaces    to foreign functions, services, components, or low-level machine    resources    * Software-Development Techniques: algorithms and data structures;    design patterns; specification; verification; validation; proof    assistants; debugging; testing; tracing; profiling    * Foundations: formal semantics; lambda calculus; rewriting; type    theory; monads; continuations; control; state; effects; program    verification; dependent types    * Analysis and Transformation: control-flow; data-flow; abstract    interpretation; partial evaluation; program calculation    * Applications and Domain-Specific Languages: symbolic computing;    formal-methods tools; artificial intelligence; systems programming;    distributed-systems and web programming; hardware design; databases;    XML processing; scientific and numerical computing; graphical user    interfaces; multimedia programming; scripting; system    administration; security    * Education: teaching introductory programming; parallel programming;    mathematical proof; algebra    * Functional Pearls: elegant, instructive, and fun essays on    functional programming    * Experience Reports: short papers that provide evidence that    functional programming really works or describe obstacles that have    kept it from working    If you are concerned about the appropriateness of some topic, do not  hesitate to contact the program chair.    Abbreviated instructions for authors  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~    * By Thursday, 28 March 2013, 23:59 UTC-11 (American Samoa time),    submit a full paper of at most 12 pages (6 pages for an Experience    Report), including bibliography and figures.    The deadlines will be strictly enforced and papers exceeding the page  limits will be summarily rejected.    * Authors have the option to attach supplementary material to a submission,    on the understanding that reviewers may choose not to look at it.    * Each submission must adhere to SIGPLAN's republication policy, as    explained on the web at    http://www.acm.org/sigplan/republicationpolicy.htm    * Authors of resubmitted (but previously rejected) papers have the    option to attach an annotated copy of the reviews of their previous    submission(s), explaining how they have addressed these previous    reviews in the present submission.  If a reviewer identifies    him/herself as a reviewer of this previous submission and wishes to    see how his/her comments have been addressed, the program chair will    communicate to this reviewer the annotated copy of his/her previous    review.  Otherwise, no reviewer will read the annotated copies of    the previous reviews.    Overall, a submission will be evaluated according to its relevance,  correctness, significance, originality, and clarity.  It should  explain its contributions in both general and technical terms, clearly  identifying what has been accomplished, explaining why it is  significant, and comparing it with previous work.  The technical  content should be accessible to a broad audience.  Functional Pearls  and Experience Reports are separate categories of papers that need not  report original research results and must be marked as such at the  time of submission.  Detailed guidelines on both categories are on the  conference web site.    Proceedings will be published by ACM Press.  Authors of accepted  submissions are expected to transfer the copyright to the  ACM.  Presentations will be videotaped and released online if the  presenter consents.    Formatting: Submissions must be in PDF format printable in black and  white on US Letter sized paper and interpretable by  Ghostscript. Papers must adhere to the standard ACM conference format:  two columns, nine-point font on a ten-point baseline, with columns  20pc (3.33in) wide and 54pc (9in) tall, with a column gutter of 2pc  (0.33in).  A suitable document template for LaTeX is available:  http://www.acm.org/sigs/sigplan/authorInformation.htm    Submission: Submissions will be accepted on the web at  https://www.easychair.org/conferences/?conf=icfp2013 . Improved  versions of a paper may be submitted at any point before the  submission deadline using the same web interface.    Author response: Authors will have a 72-hour period, starting at 0:00  UTC-11 on Wednesday, 22 May 2013, to read reviews and respond to them.    Special Journal Issue: There will be a special issue of the Journal of  Functional Programming with papers from ICFP 2013.  The program  committee will invite the authors of select accepted papers to submit  a journal version to this issue.      General Chair:    Greg Morrisett, Harvard University    Program Chair:    Tarmo Uustalu, Institute of Cybernetics, Tallinn    Program Committee:    Thorsten Altenkirch, University of Nottingham    Olaf Chitil, University of Kent    Silvia Ghilezan, University of Novi Sad    Michael Hanus, Christian-Albrechts-Universität zu Kiel    Fritz Henglein, University of Copenhagen      Mauro Jaskelioff, Universidad Nacional de Rosario    Alan Jeffrey, Alcatel-Lucent Bell Labs    Shin-ya Katsumata, Kyoto University    Shriram Krishnamurthi, Brown University    John Launchbury, Galois      Ryan Newton, Indiana University    Sungwoo Park, Pohang University of Science and Technology    Sam Staton, University of Cambridge    Nikhil Swamy, Microsoft Research, Redmond, WA    Dimitrios Vytiniotis, Microsoft Research, Cambridge

[Caml-list] VSTTE 2013 - Third call for papers

CALL FOR PAPERS
Fifth Working Conference on
Verified Software: Theories, Tools, and Experiments
(VSTTE 2013)
May 17--19, 2013, Atherton, California
[https://sites.google.com/site/vstte2013/]

The Fifth IFIP Working Conference on Verified Software: Theories,
Tools, and Experiments follows a successful inaugural working
conference at Zurich in 2005 followed by conferences in Toronto
(2008), Edinburgh (2010), and Philadelphia (2012). The goal of this
conference is to advance the state of the art in the science and
technology of software verification, through the interaction of theory
development, tool evolution, and experimental validation.

Scope: We welcome submissions describing significant advances in the
production of verified software, i.e., software that has been proved
to meet its functional specifications. We are especially interested
in submissions describing large-scale verification efforts that
involve collaboration, theory unification, tool integration, and
formalized domain knowledge. We welcome papers describing novel
experiments and case studies evaluating verification techniques and
technologies. Topics of interest include education, requirements
modeling, specification languages, specification/verification
case-studies, formal calculi, software design methods, automatic code
generation, refinement methodologies, compositional analysis,
verification tools (e.g., static analysis, dynamic analysis, model
checking, theorem proving, satisfiability), tool integration,
benchmarks, challenge problems, and integrated verification
environments.

Submission: We are accepting both long (limited to 20 pages) and short
(limited to 12 pages) paper submissions. Short submissions also cover
Verification Pearls describing an elegant proof or proof technique.
Submitted research papers and system descriptions must be original and
not submitted for publication elsewhere. Research paper submissions
must be in LNCS format and must include a cogent and self-contained
description of the ideas, methods, results, and comparison to existing
work. Submissions of theoretical, practical, and experimental
contributions are equally encouraged, including those that focus on
specific problems or problem domains.

Papers can be submitted at https://www.easychair.org/conferences/?conf=vstte2013.
Submissions that arrive late, are not in the proper format, or are too
long will not be considered. The post-conference proceedings of VSTTE
2013 will be published by Springer-Verlag in the LNCS series. Authors
of accepted papers will be requested to sign a form transferring
copyright of their contribution to Springer-Verlag. The use of LaTeX
and the Springer llncs class files, obtainable from
http://www.springer.de/comp/lncs/authors.html, is strongly encouraged.

Important Dates:
Feb 22, 2013 (firm): Title/Abstract
Mar 1, 2013 (firm): Full paper submission
Mar 29, 2013: Decision
May 17--19, 2013: Conference
Jun 28, 2013 (firm): Camera-ready

School/Workshops: The conference will be colocated with the Third Summer School
on Formal Techniques, and is preceded by NFM 2013 at NASA Ames
and followed by ICSE 2013 at San Francisco.

Conference Chair: Natarajan Shankar, SRI International

Program Chairs: Ernie Cohen, Microsoft, Andrey Rybalchenko, TU Munich

Program Committee: Josh Berdine, Ahmed Bouajjani, Marsha Chechik,
Jean-Christophe Filliatre, Silvio Ghilardi, Aarti Gupta, Arie Gurfinkel,
Andrew Ireland, Ranjit Jhala, Cliff Jones, Rajeev Joshi, Gerwin Klein,
Daniel Kroening, Gary Leavens, Xavier Leroy, Zhiming Liu, Pete
Manolios, Tiziana Margaria, David Monniaux, Peter Mueller, David
Naumann, Aditya Nori , Peter O'Hearn, Matthew Parkinson, Wolfgang
Paul, Andreas Podelski, Zhong Shao, Willem Visser, Thomas Wies, Jim
Woodcock, Kwangkeun Yi, Pamela Zave, Lenore Zuck

Publicity Chair: Sam Owre, SRI International

Steering Committee: Tony Hoare, Andrew Ireland, Jay Misra, Natarajan
Shankar, Jim Woodcock

--
Caml-list mailing list. Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs