The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

Hi all

Further to Adam's message: it was me (Andrew Kennedy) who has suggested a 
short session on "computation" inside Coq developments. Recently I've been 
using Coq to model, generate, and reason about x86 machine code - all inside 
Coq with no use of extraction or external tools. Naturally this involves 
significant use of *execution* inside the Coq environment. I wonder if anyone 
else has a similar experience to report, problems with this "mode-of-abuse" 
of Coq that they would like to overcome, or alternative approaches. Please 
let me know if you would like to contribute to this discussion, perhaps 
presenting a short overview at the workshop.

Cheers
Andrew.

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Adam Chlipala
Sent: 30 June 2012 16:06
To: 
coq-club AT inria.fr
Subject: [Coq-Club] Coq Workshop call for participation in discussion sessions

This year's Coq Workshop <http://coq.inria.fr/coq-workshop/2012> is shaping 
up well; we have enough proposals for great presentations and discussions 
that the available time is starting to look a bit tight. :) I should, in the 
not too distant future, get a concrete schedule up on the workshop web site, 
but here's a summary of what the program committee is thinking:

- 2 invited talks, one on univalent foundations in Coq, plus the customary 
talk from the Coq team, updating us on the latest developments
- 8 contributed talks (3 more from a later round not yet included on the web 
site)
- 2 of the contributed talks came with suggestions that they might be 
expanded into discussion sessions, which leads into...

We are tentatively planning two thematic sessions, ideally with multiple 
short presentations and then plenty of time for discussion.  Each has one 
initial proposer who has signed on for a short talk, with room for more.  The 
topics are:
* Coq in university teaching
* Taking advantage of computation inside Coq developments, rather than just 
via extraction

I would like to ask anyone interested in contributing to one of these 
sessions to either contact me or just reply to coq-club with ideas, according 
to your preference.