http:^^www.cs.cornell.edu^info^people^jyh^prl-seminar.html
来自「This data set contains WWW-pages collect」· HTML 代码 · 共 77 行
HTML
77 行
MIME-Version: 1.0
Server: CERN/3.0
Date: Sunday, 01-Dec-96 20:31:26 GMT
Content-Type: text/html
Content-Length: 2728
Last-Modified: Thursday, 01-Aug-96 17:12:28 GMT
<html>
<head>
<title>PRL Seminar talks</title>
</head>
<!--comment-->
<body>
<h1>PRL Seminars</h1>
<p>
Here are some of the slides for the talks I have given in the Nuprl
seminar. These slides can be pretty technical, and assume knowledge
of the Nuprl system and type theory. In some cases I
present information at an intuitive level that is technically imprecise.
<p>
All slides are in Portable Document Format (PDF). You can obtain a
PDF reader from <a
href="http://www.adobe.com/acrobat/readstep.html">Adobe</a> for just about any machine you
can imagine using. I prepared these presentations using <a
href="http://www.adobe.com/prodindex/persuasion/main.html">Adobe
Persuasion</a> and <a
href="http://www.adobe.com/prodindex/illustrator/main.html">Adobe Illustrator</a>.
<ul>
<li>
<!WA0><!WA0><!WA0><!WA0><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/mod2_96.pdf">Modules</a> February, 1996. This is
my most recent version of formal modules and objects.
<li>
<!WA1><!WA1><!WA1><!WA1><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/mod10_95.pdf">Modules</a> October, 1995. This
is an earlier version of formal modules.
<li>
<!WA2><!WA2><!WA2><!WA2><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/hor11_95.pdf">Horus</a> November, 1995. We
are performing a verification of the <a
href="http://simon.cs.cornell.edu/Info/Projects/HORUS/">Horus group
communication system</a>. These slides give an outline of the
verification process.
<li>
<!WA3><!WA3><!WA3><!WA3><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/typ10_94.pdf">Types</a> October, 1994. These
slides cover some new type additions I was proposing for Nuprl. This
includes very-dependent function types.
<li>
<!WA4><!WA4><!WA4><!WA4><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/sqrt5_94.pdf">Square Root Verification</a>
May, 1994. This talk is about the verification of a hardware square
root algorithm by program transformation. The slides don't contain
much explanation. The <!WA5><!WA5><!WA5><!WA5><a href="http://www.cs.cornell.edu/Info/People/jyh/papers/tpcd94.ps">paper</a> we wrote
for <!WA6><!WA6><!WA6><!WA6><a href="http://goethe.ira.uka.de/tpcd94/toc.html">TPCD 1994</a>
(Theorem Provers in Circuit Design) is a better resource.
<li>
<!WA7><!WA7><!WA7><!WA7><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/thy3_94.pdf">Theories</a> March, 1994. This
is a very early version of formal theories (modules) in Nuprl.
<li>
<!WA8><!WA8><!WA8><!WA8><a href="http://www.cs.cornell.edu/Info/People/jyh/nuprl/seminars/vote11_93.pdf">Majority Vote</a> November,
1993. This is the first formalization I did in Nuprl. I gives some
idea of the problems I first encountered using Nuprl, and it provides
motivation for my current work in Nuprl.
</ul>
<h2>Some other talks.</h2>
<h3>Horus talks</h3>
<p>
<ul>
<li>
<!WA9><!WA9><!WA9><!WA9><a href="http://www.cs.cornell.edu/Info/People/jyh/horus/pi96.pdf">Horus Verification</a> January, 1996. This
is a very high-level overview of the Horus verification effort.
<li>
<!WA10><!WA10><!WA10><!WA10><a href="http://www.cs.cornell.edu/Info/People/jyh/horus/hor4_96.pdf">Horus Verification</a> April, 1996. Here
is a slightly more detailed, but still high-level, version of the Horus verification.
</ul>
</body>
⌨️ 快捷键说明
复制代码Ctrl + C
搜索代码Ctrl + F
全屏模式F11
增大字号Ctrl + =
减小字号Ctrl + -
显示快捷键?