anchor.diff:  Mathematics_. Invited paper, EUROCAL85, April 1985, Linz, Austria. Springer Verlag
   LNCS 203, pp. 151-184.
   
  -Christine Paulin joined the team at this point, for her DEA research internship.
  -In her DEA memoir (August 1985) she presents developments for the _lambo_ function
  -computing the minimal _m_ such that _f(m)_ is greater than _n_, for _f_ an increasing
  -integer function, a challenge for constructive mathematics. She also encoded
  +Christine Paulin joined the team at this point, for her DEA research
  +internship.  In her DEA memoir (August 1985) she presents developments
  +for the _lambo_ function – _lambo(f)(n)_ computes the minimal _m_ such
  +that _f(m)_ is greater than _n_, for _f_ an increasing integer
  +function, a challenge for constructive mathematics. She also encoded
   the majority voting algorithm of Boyer and Moore.
   
   Version 2
  
positive.code: Science, 1993.
  
  The last version of CONSTR is Version 4.11, which was last distributed
  in Spring 1990. It was demonstrated at the first workshop of the European
  Basic Research Action Logical Frameworks In Sophia Antipolis in May 1990.
  
  At the end of 1989, Version 5.1 was started, and renamed as the system Coq
  
negative.code: Version 4.5 was demonstrated in June 1988 at the YoP Institute on Logical
  Foundations of Functional Programming organized by Gérard Huet at Austin, Texas.
  
  Version 4.6 was started during the summer of 1988. Its main improvement was the
  complete rehaul of the proof synthesis engine by Thierry Coquand, with
  a tree structure of goals.
  
  