Speaker:

  Renaud Rioboo
  Universite Pierre et Marie Curie 

Title:

  Concrete Mathematics with the FoCaL Environment

Abstract:

  In this talk we will present some new features of the FoCaL
  language.  We will first start by recalling the basic concepts of
  specie and collection defined by the FoCaL (formerly FoC) project.
  We will then present the FoCaL proof language which enables one to
  perform proofs which are very close to hand written proofs.  Proofs
  performed in the FoCaL proof language are then analyzed by the Zenon
  proof guesser in order to check their correctness and finally
  transformed into proofs which are checked again by the Coq proof
  assistant.

  Some concrete results in basic commutative algebra will be
  illustrated in the talk and some ongoing work with other Calculemus
  community members about effective algebraic topology will be
  presented.