[TYPES] Calculemus 2005 Call for Participation

[William Farmer]

			CALL FOR PARTICIPATION

			   Calculemus 2005
				   
	       In conjunction with Formal Methods 2005

	  University of Newcastle upon Tyne, United Kingdom
			   July 18-19, 2005

	       http://imps.mcmaster.ca/calculemus-2005/

The Calculemus Interest Group (http://www.calculemus.net/) is
dedicated to advancing the integration of symbolic computation and
formal deduction in mathematical software systems and computer-aided
verification tools.  Calculemus has previously sponsored a series of
11 symposia starting in 1996 whose aim is to bring together
researchers interested in this objective.  (Calculemus was also part
of IJCAR 2004.)  This series is the major forum for the presentation
of research in combining the capabilities of computer algebra systems
and computer deduction systems.

Calculemus 2005, the 12th symposium in the series, will be held July
18-19, 2005 at the University of Newcastle upon Tyne, United Kingdom
in conjunction with Formal Methods 2005.  A principal theme of
Calculemus 2005 will be interactions with formal methods, including
problems in formal methods which require a mixture of computing and
proving, and applications of formal methods to the construction of
integrated systems.

PROGRAM

Invited Talks

  Natarajan Shankar (SRI International)
  "Explaining Decision Procedures"

  Renaud Rioboo (Universit'e Pierre et Marie Curie)
  "Concrete Mathematics with the FoCaL Environment"

Paper Presentations

  Lu'is Cruz-Filipe (Instituto Superior T'echnico) and 
     Pierre Letouzey (LMU Munich)
  "A Large-Scale Experiment in Executing Extracted Programs"

  Martin Pollet (Univ. Saarland) and Volker Sorge (Univ. Birmingham)
  "Connecting Logical Representations and Efficient Computations"

  J"orn Ossowski and Christel Baier (Univ. Bonn)
  "Symbolic Reasoning with Weighted and Normalized Decision Diagrams"

  Ruth Anne Hardy (Univ. St. Andrews)
  "Interactions between PVS and Maple in Symbolic Analysis of Control 
     Systems"

  Tobias Schmidt-Samoa (Tech. Univ. Kaiserslautern)
  "An Even Closer Integration of Linear Arithmetic into Inductive Theorem 
     Proving"

  David Delahaye (CNAM) and Micaela Mayero (Univ. Paris Nord)
  "Quantifier Elimination over Algebraically Closed Fields in a Proof 
     Assistant using a Computer Algebra System"

  Aur'elie Hurault and Marc Pantel (IRIT)
  "Mathematical Service Trading Based on Equational Matching"

  Geoff W. Hamilton (Dublin City Univ.)
  "Poit'in: Distilling Theorems From Conjectures"

  Roy L. McCasland (Univ. of Edinburgh), Alan Bundy (Univ. of Edinburgh), 
     and Patrick F. Smith (Univ. of Glasgow)
  "Ascertaining Mathematical Theorems"

  Louise A. Dennis (Univ. Nottingham), Mateja Jamnik (Univ. Cambridge), 
    and Martin Pollet (Univ. Saarland)
  "On the Comparison of Proof Planning Systems LambdaClam, Omega 
     and IsaPlanner"

SYMPOSIUM AND PROGRAM CHAIRS

Jacques Carette      McMaster University, Canada
William M. Farmer    McMaster University, Canada

PROGRAM COMMITTEE

Andrew A. Adams      University of Reading, UK
Alessandro Armando   Universit`a di Genova, Italy
Michael Beeson       San Jose State University, USA
Wieb Bosma           Radboud Universiteit Nijmegen, The Netherlands
Manuel Bronstein     INRIA Sophia Antipolis, France
Jacques Calmet       Universit"at Karlruhe, Germany
J"urgen Gerhard      Maplesoft, Canada
Michael Kohlhase     International University Bremen, Germany
Marc Moreno Maza     University of Western Ontario, Canada
Roy McCasland        University of Edinburgh, UK
Silvio Ranise        LORIA and INRIA Lorraine, France
Piotr Rudnicki       University of Alberta, Canada
Volker Sorge         University of Birmingham, UK
Adam Strzebonski     Wolfram Research, USA
Volker Weispfenning  Universit"at Passau, Germany

Please send questions to:

Jacques Carette (carette at mcmaster.ca)
William M. Farmer (wmfarmer at mcmaster.ca)