Le 13 août 12 à 21:13, Bill Richter a écrit :
http://plato.stanford.edu/entries/type-theory/ by Thierry Coquand
(associated with Coq), and
http://plato.stanford.edu/entries/type-theory-church/ by Peter
Andrews
Cris, these look really good! Are you telling me that the term Coq
comes from Thierry Coquand's name?
"Coq" is both a reference to the "Calculus of Constructions" ("CoC")
which is the type system underlying Coq, and a kind of tribute to
Thierry Coquand who introduced this type system.
--
Vincent Aravantinos
PostDoctoral fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
