On 14/08/12 14:30, Cris Perdue wrote:
> I prefer not to say that a type is a set, because the set of all
> things having a type is expressible as \x. T (or {x | T}.
> Cris, I'm tempted to go with Michael, who sorta disagreed with
> you above. Let me try to resolve the semi
On Mon, Aug 13, 2012 at 6:05 PM, Bill Richter wrote:
> Michael, Konrad, Rob, Mark, Cris, thank you very much for all the
> messages! This partly answers many questions that have puzzled me. Among
> other things, I'm well on way to having to give you guys acknowledgments in
> my paper. I think
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
> Konrad, this is very interesting, because it's so much like sets.ml:
>
>There is also a description of sets in HOL4 in the manual. Start at
>p. 102 of the HOL4 Description document:
>
> Yours & Michael's Description manual starts pretty much like sets.ml which I
> cited above.
Not surpr
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?
--
Best,
Bill
-
Michael, Konrad, Rob, Mark, Cris, thank you very much for all the messages!
This partly answers many questions that have puzzled me. Among other things,
I'm well on way to having to give you guys acknowledgments in my paper. I
think the point of an acknowledgment isn't to pay someone for help
[Note: Submission Deadline is 19 September 2012]
7th Systems Software Verification Conference (SSV 2012)
November 28--30, 2012
Sydney, Australia
http://www.ssv-conference.org/
*Scope
Industrial-strength software analysis and v
Bill,
On Sun, Aug 12, 2012 at 9:53 PM, Bill Richter wrote:
> Thanks, Mark! I looked at Tom Hales's Notices article, as you suggested
> www.ams.org/notices/200811/tx081101370p.pdf
> Now Tom is a great mathematician (he's the main reason I'm here), but Tom
> is now an HOL Light expert, and I thin
>> Does HOL4 have anything comparable to sets.ml?
> Yes it will have, and it will probably be spread over many source code
> files, but I'm afraid I don't know where this is in the HOL4 source. This
> is a question for HOL4 community, Michael et al. I'm more of a HOL Light
> and HOL Zero person.
Our apologies if you have received multiple copies.
##
CALL FOR PAPERS
Fifth International Conference on
Fundamentals of Software Engineering 2013
Theory and Practice
(FSEN '13)
http://fsen.ir/2013
Tehran, Iran
April 24-
On 13 Aug 2012, at 00:53, Bill Richter wrote:
>
> What is a type?
>
If you have time to look at a textbook reference as background to all this,
here is a good one describing a system that is very similar in spirit to HOL.
@BOOK{andrews,
author = "Peter B. Andrews",
11 matches
Mail list logo
