[TYPES] Calculemus 2005 Call for Participation
wmfarmer at mcmaster.ca
Tue Jun 14 16:53:10 EDT 2005
CALL FOR PARTICIPATION
In conjunction with Formal Methods 2005
University of Newcastle upon Tyne, United Kingdom
July 18-19, 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
Natarajan Shankar (SRI International)
"Explaining Decision Procedures"
Renaud Rioboo (Universit'e Pierre et Marie Curie)
"Concrete Mathematics with the FoCaL Environment"
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
Tobias Schmidt-Samoa (Tech. Univ. Kaiserslautern)
"An Even Closer Integration of Linear Arithmetic into Inductive Theorem
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
SYMPOSIUM AND PROGRAM CHAIRS
Jacques Carette McMaster University, Canada
William M. Farmer McMaster University, Canada
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)
More information about the Types-list