Calculemus 2008: extended deadline March 14

Dear colleagues,

Calculemus 2008 was announced to close the submission process
on March 7, 2008, but now has a new

    ***extended deadline of March 14, 2008.***

The second CFP follows. More information in:

  http://events.cs.bham.ac.uk/calculemus08/

+++++++++++++

[apologies for multiple postings]

Second Call for Papers (with extended deadline)

--------------------------
C A L C U L E M U S   2008
--------------------------

July 30 -- August 1, 2008

University of Birmingham, UK

http://events.cs.bham.ac.uk/calculemus08/

General
-------
Calculemus is a series of conferences dedicated to the

2nd CFP: PLMMS 2008

                          SECOND CALL FOR PAPERS

  * UPDATE: Post-workshop proceedings in Journal of Automated Reasoning
  * UPDATE: Invited talk by Conor McBride

                            Second Workshop on
             Programming Languages for Mechanized Mathematics
                              (PLMMS 2008)

          http://events.cs.bham.ac.uk/cicm08/workshops/plmms/

                        As part of CICM / Calculemus 2008
                     Birmingham, UK, 28-29 July 2008

This workshop is focused on the intersection of programming languages
(PL) and mechanized mathematics systems (MMS). The latter category
subsumes present-day computer algebra systems (CAS), interactive proof
assistants (PA), and automated theorem provers (ATP), all heading
towards fully integrated mechanized mathematical assistants that are
expected to emerge eventually (cf. the objective of Calculemus).

The two subjects of PL and MMS meet in the following topics, which are
of particular interest to this workshop:

  * Dedicated input languages for MMS: covers all aspects of languages
    intended for the user to deploy or extend the system, both
    algorithmic and declarative ones. Typical examples are tactic
    definition languages such as Ltac in Coq, mathematical proof
    languages as in Mizar or Isar, or specialized programming

TTVSI registration deadline

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/

_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: TTVSI early registration deadline

Call For Bids (TPHOLs'09) --Deadline extension (March 25, 2008)--

--Apologies if you receive this e-mail several times--

CALL FOR BIDS

22nd International Conference
on Theorem Proving in Higher Order Logics

It is time to begin the process of selecting a host for TPHOLs 2009. As is
the tradition, the hosts of the previous conference (i.e. TPHOLs 2008) are
running the process. There are two phases: solicitation of bids and voting.
This message concerns the first phase.
A longstanding convention is that the conference should be held in a
continent different to the location of the previous meeting, and therefore
no bids to host TPHOLs 2009 in America will be accepted. TPHOLs is
traditionally held in August or September. Bids should be sent to
tphols08 <at> ece.concordia.ca and should  include at least the following
information:

name and email address of a contact person :
names of other people involved             :
address of website for the bid             :
approximate dates the conference           :
format of the conference                   :

Previous bids can be accessed through the TPHOLs webpages. Please refer to
the TPHOLs 2009 Host Selection page

http://www.ece.concordia.ca/TPHOLs2008/tphols2009.php

Deadline for all bids is 25 March 2008.

Shortly after that, the bids will be made public and the voting phase will
take place. The people eligible to vote are those who are seriously
thinking of attending TPHOLs 2009. The voting system used will be Single
Transferable Vote between all received bids.

--

-- 
TPHOLs'08 organizing committee.

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/

ML Workshop 2008 call for papers

                           CALL FOR PAPERS

                 The 2008 ACM SIGPLAN Workshop on ML

                      Sunday, September 21, 2008
                  Victoria, British Columbia, Canada
               To be held in conjunction with ICFP 2008

               http://www.kb.ecei.tohoku.ac.jp/ml2008/

IMPORTANT DATES:

Submission deadline:        Monday, June 23, 2008
Notification of acceptance: Friday, July 18, 2008
Final revision due:         Monday, July 28, 2008
Workshop:                   Sunday, September 21, 2008

GOALS OF THE WORKSHOP:

ML is a family of programming languages that includes dialects known
as Standard ML, Objective Caml, and F#.  The development of these
languages has inspired a large amount of computer science research,
both practical and theoretical.  This workshop aims to build on
previous occasions (recent instances are ML 2005 in Tallinn, Estonia,
2006 in Portland, Oregon, and 2007 in Freiburg, Germany), providing a
forum to encourage discussion and research on ML and related
technology.

The 2008 Workshop on ML will be held in conjunction with the 13th ACM
SIGPLAN International Conference on Functional Programming (ICFP 2008)
in Victoria, British Columbia, Canada on Sunday, September 21, 2008.

This year we extend the scope of the workshop from ML itself to
technologies closely related to ML (higher-order, typed, or strict
languages) and invite high-quality papers in all areas of crucial
importance for the future of ML.

SUBMISSION GUIDELINES:

We seek papers on topics related to ML, including (but not limited
to):

 * applications

 * extensions: objects, classes, concurrency, distribution and
   mobility, semi-structured data handling, etc.

 * type systems (static and dynamic): inference, effects, overloading,
   error reporting, contracts, specifications and assertions, etc.

 * implementation: compilers, interpreters, partial evaluators,
   garbage collectors, etc.

 * environments: libraries, tools, editors, debuggers, cross-language
   interoperability, functional data structures, etc.

 * semantics

Submitted papers should describe new ideas, experimental results,
ML-related projects, or informed positions regarding proposals for
next-generation ML languages.  In order to encourage lively
discussion, submitted papers may describe work in progress.  All
papers will be judged on a combination of correctness, significance,
novelty, clarity, and interest to the community.

All paper submissions must be at most 12 pages total length in the
standard ACM SIGPLAN two-column conference format (9pt):

        http://www.acm.org/sigs/sigplan/authorInformation.htm

Accepted papers will be published by the ACM and will appear in the
ACM Digital Library.

More details about the submission procedure will be announced later on
the web page:

        http://www.kb.ecei.tohoku.ac.jp/ml2008/

PROGRAM CHAIR:

Eijiro Sumii     (Tohoku University)

PROGRAM COMMITTEE:

Sylvain Conchon  (Paris-Sud University / INRIA Saclay-Ile-de-France)
Karl Crary       (Carnegie Mellon University)
Andrzej Filinski (DIKU)
Robby Findler    (The University of Chicago)
Cormac Flanagan  (University of California at Santa Cruz)
Alain Frisch     (LexiFi)
Dan Grossman     (University of Washington)
Didier Remy      (INRIA Paris-Rocquencourt)
Claudio Russo    (Microsoft Research Cambridge)
Eijiro Sumii     (Tohoku University)
Hongwei Xi       (Boston University)

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/

SPIN 2008: Final Call for Papers

 *******************************************************
                Final Call for Papers: SPIN 2008

 15th Int. SPIN Workshop on Model Checking of Software
                       August 10-12, 2008
                   University of California

                     Los Angeles, USA

              http://compilers.cs.ucla.edu/spin08
 *******************************************************

 Aim and Scope:

 The SPIN workshop is a forum for practitioners and researchers
 interested in state space-based techniques for the validation and
 analysis of software systems. Theoretical techniques and empirical
 evaluations based on explicit representations of state spaces, as
 implemented in the SPIN model checker or other tools, or techniques
 based on combination of explicit representations with other
 representations, are the focus of this workshop.

 We particularly welcome papers describing the development and
 application of state space exploration techniques in testing and
 verifying security-critical software, enterprise and web applications,
 embedded software, and other interesting software platforms. The
 workshop aims to encourage interactions and exchanges of ideas with all
 related areas in software engineering.

 Invited speakers:

 - Matthew Dwyer (University of Nebraska)
 - Daniel Jackson (MIT)
 - Shaz Qadeer (Microsoft Research)
 - Wolfram Schulte (Microsoft Research)
 - Yannis Smaragdakis (University of Oregon)

 Important Dates and Deadlines:

 Deadline for submission of full papers: April 2, 2008
 Notification of acceptance/rejection: May 10, 2008.
 Deadline for final version of accepted papers: May 28, 2008.
 Workshop: August 10-12, 2008.

 Topics of Interest:

 - Algorithms and storage methods for explicit state model checking
 - Directed model checking using heuristics
 - Parallel or distributed model checking using multi-core or
multiple computers
 - Techniques for dealing with infinite state spaces
 - Model checking of timed and probabilistic systems
 - Abstraction and the use of static analysis to reduce state spaces
 - Combinations of enumerative and symbolic techniques
 - Analysis for modeling languages, including SE languages (UML,...)
 - New property specification languages, including new forms of temporal logic
 - Model checking of programming languages and code analysis
 - Automated testing using model checking techniques
 - Derivation of invariants, test cases, or other useful information
 from state spaces
 - Combination of model-checking techniques with other analysis techniques
 - Modularity and compositionality
 - Comparative studies, including to other model checking techniques
 - Case studies of interesting systems or with interesting results
 - Theoretical and algorithmic foundations of model-checking based analysis
 - Engineering and implementation of model-checking tools and platforms
 - Insightful surveys or historical accounts on topics of relevance to
 SPIN workshops

 Solicited Contributions:

 With the exception of survey and history papers, the papers should
 contain original work which has not been submitted or accepted for
 publication elsewhere. Submissions should adhere to the LNCS format. We
 solicit two kinds of papers:

 1. Technical Papers.  No longer than 18 pages in LNCS format. All
 accepted technical papers will be included in the proceedings.

 2. Tool Presentations. This kind of submissions should consist of two
 parts. The first part is at most 5 page description of the tool. If
 accepted, this part will be published in the workshop proceedings. The
 second part should describe an informal plan for an oral presentation of
 the tool. This part will not be included in the proceedings.

 The proceedings of SPIN usually appear in Springer's Lecture Notes in
 Computer Science series. We expect to continue this tradition for
 the 2008 edition.

 Organization:

 General Chair:

 Jens Palsberg (UC Los Angeles, USA)

 Programme Chairs:

 Klaus Havelund (NASA JPL/Caltech., USA)
 Rupak Majumdar (UC Los Angeles, USA)

 Programme Committee:

 Christel Baier  (Bonn, Germany)
 Dragan Bosnacki (Eindhoven, Netherlands)
 Lubos Brim (Brno, Czech)
 Stefan Edelkamp (Dortmund, Germany)
 Dawson Engler (Stanford, USA)
 Kousha Etessami (Edinburgh, UK)
 Susanne Graf (Verimag, France)
 John Hatcliff (Kansas State Univ., USA)
 Gerard Holzmann (NASA JPL, USA)
 Franjo Ivancic (NEC, USA)
 Sarfraz Khurshid (UT Austin, USA)
 Kim Larsen (Aalborg, Denmark)
 Madan Musuvathi (Microsoft, USA)
 Joel Ouaknine (Oxford, UK)
 Corina Pasareanu (NASA Ames, USA)
 Doron Peled (Warwick, UK)
 Paul Pettersson (Malardalen, Sweden)
 Koushik Sen (Berkeley, USA)
 Natasha Sharygina (Lugano, Switzerland)
 Eran Yahav (IBM, USA)

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/

Announcing SMT-COMP 2008

======================================================================

                          CAV'08 Satellite Event

       4th International Satisfiability Modulo Theories Competition
                               (SMT-COMP'08)

                              Princeton, USA
                                 July 2008

                            CALL FOR BENCHMARKS
                             CALL FOR ENTRANTS

======================================================================

Decision procedures for checking satisfiability of logical formulas
are crucial for many verification applications.  Of particular recent
interest are solvers for Satisfiability Modulo Theories (SMT).
SMT-COMP aims to spur innovation in SMT research by providing a yearly
friendly competition for SMT solvers.

SMT-COMP came out of discussions surrounding the SMT-LIB initiative,
an initiative of the SMT community to build a library of SMT
benchmarks in a proposed standard format.  SMT-COMP helps serve this
goal by contributing collected benchmark formulas used for the
competition to the library, and by providing an incentive for
implementors of SMT solvers to support the SMT-LIB format.

As part of SMT-COMP 2007, a special session was held at SMT Workshop
2007 in which the competitors had a chance to present their tools and
discuss them with other competitors.  This year, a similar session
will be held as part of SMT Workshop 2008 (July 7-8, affiliated with
CAV).  More information about the SMT Workshop can be found on the web
page: http://research.microsoft.com/conferences/SMT08/

The highlights of SMT-COMP 2008 are covered below.  For the latest
information, please see the SMT-COMP web page at:

http://www.smtcomp.org/

------------------------------------------
Main changes with respect to SMT-COMP 2007
------------------------------------------

- Use of the SMT-EXEC services for solver submission and execution

- Updates to the benchmark selection algorithms

- Additional mechanisms for transparency and reproducibility of results

- Existence of a two-day grace period for bug fixing

For more detailed information please refer to the rules posted at
http://www.smtcomp.org/.

---------------
Benchmarks
---------------

The potential benchmark divisions for this year include all of the
divisions represented last year. We do not anticipate new divisions
this year unless quality benchmarks are collected. For detailed
descriptions of the divisions, refer to the SMT-LIB web page at
http://www.smtlib.org/

* QF_UF (Uninterpreted Functions): quantifier-free formulas whose
  satisfiability is to be decided modulo the empty theory. Each
  benchmark may introduce its own uninterpreted function and predicate
  symbols.

* QF_IDL (Integer Difference Logic): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of integer
  arithmetic.  The syntax of atomic formulas is restricted to
  difference logic, i.e. x - y op c, where op is either equality or
  inequality and c is an integer constant.

* QF_RDL (Real Difference Logic): this division is like QF_IDL, except
  that the background theory is real arithmetic.

* QF_UFIDL (Integer Difference Logic with Uninterpreted Functions):
  this division contains benchmarks in a logic which is similar to
  QF_IDL, except that it also allows uninterpreted functions and
  predicates.

* QF_LIA (Linear Integer Arithmetic): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of integer
  arithmetic.  The syntax of atomic formulas is restricted to contain
  only linear terms.

* QF_LRA (Linear Real Arithmetic): this division is like QF_LIA,
  except that the background theory is real arithmetic.

* QF_UFLIA (Linear Integer Arithmetic with Uninterpreted Functions):
  this division contains benchmarks in a logic which is similar to
  QF_LIA, except that it also allows uninterpreted functions and
  predicates.

* QF_AX (Arrays with Extensionality): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of arrays which
  includes the extensionality axiom.

* QF_AUFLIA (Linear Integer Arithmetic with Uninterpreted Functions
  and Arrays): quantifier-free formulas to be tested for
  satisfiability modulo a background theory combining linear integer
  arithmetic, uninterpreted function and predicate symbols, and
  extensional arrays.

* QF_BV (Fixed-size Bit-vectors): quantifier-free formulas over bit
  vectors of fixed size.

* QF_AUFBV (Bit-vectors with Arrays and Uninterpreted Functions):
  quantifier-free formulas over bit vectors of fixed size, with arrays
  and unintepreted functions and predicate symbols.

* AUFLIA+p (Linear Integer Arithmetic with Uninterpreted Functions and
  Arrays): quantified formulas to be tested for satisfiability modulo
  a background theory combining linear integer arithmetic,
  uninterpreted function and predicate symbols, and extensional
  arrays. Benchmarks include patterns for guiding instantiation
  mechanisms.

* AUFLIA-p (Linear Integer Arithmetic with Uninterpreted Functions and
  Arrays): formulas from AUFLIA+p once all patterns have been
  removed.

* AUFLIRA+p (Arrays, Uninterpreted Functions, and Linear Arithmetic):
  quantifier formulas with arrays of reals indexed by integers
  (Array1), arrays of Array1 indexed by integers (Array2), and linear
  arithmetic over the integers and reals. Benchmarks include patterns
  for guiding instantiation mechanisms.

* AUFLIRA-p (Arrays, Uninterpreted Functions, and Linear Arithmetic):
  formulas from AUFLIRA+p once all patterns have been removed.

As with last year, we reserve the right to remove benchmark divisions
if we do not receive enough quality benchmarks or enough solvers in a
particular division.  If you have access to benchmarks in any of these
divisions, even if they are not in the SMT-LIB format, please contact
one of the organizers (see below).

---------------
Solvers
---------------

Please refer to http://www.smtcomp.org/ for complete details on
entering the competition.

---------------
Travel Grants
---------------

Microsoft Research has generously donated funds to help pay for travel
for participants, especially students, who might otherwise be unable
to attend. Because funds are limited, we will use a bidding process to
assign grants. The process works like this:

 1. Those interested should send an email by June 1 to Clark Barrett 
 indicating:
    * Your name and affiliation.
    * Whether you are a student.
    * The name of the solver you are submitting and your role in the 
    development of the solver.
    * The amount of assistance you would need to be able to attend. 

 2. On or before June 11, we will notify those whose bids have been
    accepted (acceptance will be based primarily on the amount
    requested, with lower bids having precedence, but we will also
    take into account the role of the applicant in the development of
    the solver and whether or not the applicant is a student).

 3. Following the conclusion of the competition, reimbursement checks
    will be issued to those whose bids were accepted and who attended.

---------------
Important Dates
---------------

    * May 1:     First version of the benchmark library posted for 
                 comment.

    * June 1:    Revised version of the benchmark library posted.
      	    	 Travel grant applications due.

    * June 11:   Travel grant notification sent.

    * July 4:    Final version of solvers due via SMT-EXEC,with magic 
     (7pm ET)	 numbers for pseudo-random selection of benchmarks.

    * July 6:    Close of two-day grace period for resubmission of 
     (7pm ET) 	 entries.

    * July 7-8:  SMT Workshop.

    * July 9-13: Anticipated dates for competition.

-----------------
Organizers
-----------------

Clark Barrett   (New York University, barrett <at> cs.nyu.edu)
Morgan Deters   (Technical Univ. of Catalonia, mdeters <at> lsi.upc.edu)
Albert Oliveras (Technical Univ. of Catalonia, oliveras <at> lsi.upc.edu)
Aaron Stump     (Washington University in St. Louis, stump <at> cse.wustl.edu)

----------------
More Information
----------------

For details on the competition, see
http://www.smtcomp.org/

For more information on the SMT-LIB format, see
http://www.smtlib.org/

For more information about the SMT Workshop, see
http://research.microsoft.com/conferences/SMT08/

SMT-COMP is partially sponsored by the U.S. National Science Foundation, under
grant CNS-0551697.

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/

Program verification

Dear All,

I am interested in substantial, state-of-the-art examples of program
verification. "Program" should be interpreted quite widely, e.g. so as
to include Gonthier's four-colour theorem work, and Harrison's HOL in
HOL work. "Verification" should also be loosely interpreted, to include
very weak properties such as e.g. absence of null-pointer dereference,
as well as strong properties such as functional correctness, liveness etc.

I would be very grateful if people could reply to this message with
their favourite examples.

I will attempt to set up a wikipedia page with the information so gleaned.

Many thanks

Tom

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/

IJCAR's ESHOL Workshop - CFP

-------------------------------------------------------------------------------
                          Call for papers: ESHOL'08

The workshop

                *Evaluation of Systems for Higher Order Logic*

will be held as part of the 4th International Joint Conference on Automated
Reasoning (IJCAR'08) in Sydney, Australia.

Workshop website:     http://www.cs.miami.edu/~geoff/Conferences/ESHOL/
Workshop dates:       10/11 August 2008
Subsmission deadline: 19 May 2008 (abstract) / 26 May 2008 (full paper)

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

This workshop brings together practitioners and researchers who are involved
in the development of reasoning systems based on higher-order logic. The
workshop will stimulate and foster the build-up of an infrastructure that
supports research, development, and deployment of higher-order reasoning
systems. A particular focus is on means to evaluate higher-order reasoning
systems.  Advances in these aspects of reasoning in higher-order logic will
make higher-order reasoning system easier to use in applications, e.g.,
hardware and software verification, knowledge based reasoning, and computer
aided mathematics. The workshop's notion of higher-order includes, but is not
limited to, ramified type theory, simple type theory, intuitionistic and
constructive type theory, and logical frameworks. The workshop's notion of
reasoning systems includes automated and semi-automated provers, model
generators, as well as proof and model checkers. The workshop will have three
parts:

  *Evaluation of Higher-Order Reasoning Systems*
          o Frameworks and tools for evaluation
          o Collections of test problems
          o Problem representation languages
          o Evaluation of automated higher-order reasoning systems, in
            particular, higher-order theorem provers
          o Evaluation of interactive higher-order reasoning systems
          o Evaluation of systems working for different higher-order
            logics and varying semantics

  *Descriptions of Successful Higher-Order Reasoning Systems*
          o Logical frameworks
          o Higher-order automated theorem provers
          o Interactive proof assistants supporting the partial
            automation of higher-order logic
          o Higher-order model checkers and higher-order model generators
          o Systems that automate natural fragments of higher-order
            logic, such as monadic second-order logic
      Due to the evaluative character of the workshop, descriptions of both
      existing and novel systems are welcomed. Descriptions of existing
      systems should stress successful applications and evaluations.

  *System Demonstration and System Competition*
      The systems described in the second part will be demonstrated. Moreover,
      a first competition "happening" for automated theorem provers for simple
      type theory is planned. This competition will be similar to the CASC
      competition for first-order reasoning systems. It will exploit and test
      the TPTP problem representation language for simple type theory, which
      was recently developed by the organizers.

We envision attendees that are interested in fostering the development and
visibility of reasoning systems for higher-order logics, and the connection
between research on the various flavors of higher-order logic. We are
particularly interested in comparisons of the practical strengths of higher-
order reasoning systems and in a discusssion on the development of a higher-
order version of the TPTP. Due to the intricate nature of higher-order logic,
we are also interested in a discussion on what practical strength means in
the context of higher-order logic and how it can be measured.

*Program Committee*

  Peter Andrews   Andrea Asperti Michael Beeson Christoph Benzmuller (Co-Chair)
  Chad Brown      Gilles Dowek   Viktor Kuncak  Dale Miller
  Michael Norrish Larry Paulson  Florian Rabe (Co-Chair)
  Sandip Ray      Carsten Schurmann (Co-Chair)  Natarajan Shankar
  Geoff Sutcliffe (Co-Chair)     Josef Urban

*Submission*

Submission of papers for presentation at the workshop, and proposals for
system and application demonstrations at the workshop, are now invited.
Submissions will be reviewed, and a balanced program of high-quality
contributions will be selected. There is a 20 page limit. Long listings
of problems or computer output should be relegated to a referenced WWW site.

Submission is via EasyChair (thanks to Andrei Voronkov). The selected
contributions will be printed as workshop proceedings, and will also be
published as CEUR Workshop Proceedings <http://ceur-ws.org>.

*Important dates*

    * Abstract submission deadline - 19th May
    * Submission deadline - 26rd May
    * Papers distributed to PC - 30th May
    * Reviews due in from PC - 23rd June
    * Notification of acceptance - 27th June
    * Final versions due - 14th July
    * Workshop - 10-11th August
-------------------------------------------------------------------------------

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/