[Why3-club] constructive Why3 logic ?

2014-05-05 Thread Jean-Jacques Levy
Dear Why3 Friends! from time to time, I met difficulties in making a constructive Coq proof corresponding to a Why3 goal. Has anybody met same problem ? Must of time it comes from translation of Why3 predicates into Prop's, instead of a Coq predicate (with truth values). Then it’s hard to expr

[Why3-club] Second call for participation: summer school on programming techniques (EJCP 2014)

2014-05-05 Thread Alan Schmitt
(French version below) ÉCOLE JEUNES CHERCHEURS EN PROGRAMMATION 2014 Rennes, June 16 - June 20, 2014. Organization: Olivier Barais, Thomas Jensen, and Alan Schmitt. *New* We now propose a registration fee with no accommodations for local participants. The summer school for young researchers in