[Club2] Talks on Fri 27-Jul-2007 11:30 (Turing)

[Alexander Krauss]

... I'm forwarding the announcements to the Club2 list, in order to
reach more people who might be interested...


Dear local Isabelle enthusiasts,

for our jour fixe this Friday we will have two talks, see below.


	Makarius

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

Amine Chaieb and Makarius Wenzel:

  Context aware Calculation and Deduction --- Ring Equalities via Groebner
  Bases in Isabelle

  We address some aspects of a system architecture for mathematical
  assistants that integrates calculations and deductions by common
  infrastructure within the Isabelle theorem proving environment.
  Here calculations may refer to arbitrary extra-logical mechanisms,
  operating on the syntactic structure of logical statements.
  Deductions are devoid of any computational content, but driven by
  procedures external to the logic, following to the traditional ``LCF
  system approach''.  The latter is extended towards explicit
  dependency on abstract theory contexts, with separate mechanisms to
  interpret both logical and extra-logical content uniformly.  Thus we
  are able to implement proof methods that operate on abstract
  theories and a range of particular theory interpretations.  Our
  approach is demonstrated in Isabelle/HOL by a proof-procedure for
  generic ring equalities via Groebner Bases.

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

Makarius Wenzel and Amine Chaieb:

  SML with antiquotations embedded into Isabelle/Isar

  We report on some recent experiments with SML embedded into the
  Isabelle/Isar theory and proof language, such that the program text
  may again refer to formal logical entities via antiquotations.  The
  meaning of our antiquotations within SML text observes the different
  logical environments at compile time, link time (of theory
  interpretations), and runtime (within proof procedures).  As a
  general design principle we neither touch the logical foundations of
  Isabelle, nor the SML language implementation.  Thus we achieve a
  modular composition of the programming language and the logic within
  the Isabelle/Isar framework.  Our work should be understood as a
  continuation and elaboration of the original ``LCF system
  approach'', which has introduced ML as a programming language for
  theorem proving in the first place.

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