http:^^www.cs.cornell.edu^info^people^crary^home.html

来自「This data set contains WWW-pages collect」· HTML 代码 · 共 88 行

MIME-Version: 1.0
Server: CERN/3.0
Date: Wednesday, 20-Nov-96 19:50:17 GMT
Content-Type: text/html
Content-Length: 3897
Last-Modified: Tuesday, 19-Nov-96 16:43:24 GMT

<title>Karl Crary's home page</title>
<h1>Karl F. Crary</h1>
<address><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><a href="mailto:[e-mail]">[e-mail]</a></address>
Office Address: 4153 Upson Hall<br>
Office Phone: [phone]
<hr>
<h3>Research</h3>

Broadly speaking, my primary research interests are in type theory and the design, implementation
and semantics of programming languages.  My recent emphasis has been in the areas of subtyping,
object-oriented programming and modularity.  I am implementing a practical programming language KML
which combines these features in a functional programming language, and formulating for it a
type-theoretic semantics.
<p>

An interesting view of programming languages is as a tractable approximation to the intractably rich
world of foundational type theories, in which the whole of mathematics can be performed.  New
programming language developments often result from mapping type-theoretic constructions through an
approximation into a programming language setting, and, conversely, new paradigms in programming
languages are often not well understood until they have been formulated type-theoretically.  I am
interested in deepening our understanding of this relationship between type theory and programming
languages, particularly the issues of tractability and approximation and how they can be mitigated.
<p>

I am also interested in a model of compilation that views it as a series of translations into
"lower" intermediate calculi, where each intermediate calculus can be embedded into type theory and
the corresponding interpretation of a program is invariant under each translation.  Such a model
allows us to relate each stage of compilation to an original type-theoretic semantics, which allows
the use of standard compilation techniques and optimizations while guaranteeing safety and
correctness.  Also, careful formulation of such intermediate calculi make possible additional
optimizations that are unavailable in other compilation strategies.
<p>

My work forms part of the
<!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><a href="http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html">Nuprl</a> project here
at Cornell.  The project name comes from the Nuprl system of formal mathematics and logic, a
type theory based on the type theories of Martin-L&ouml;f that is also implemented in an automated
reasoning system.
<p>

My committee consists of
<!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><a href="http://www.cs.cornell.edu/Info/Faculty/rc/rc.html">Robert Constable</a>,
<!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><a href="http://www.cs.cornell.edu/Info/People/jgm/home.html">Greg Morrisett</a>,
and <!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><a href="http://www.cs.cornell.edu/Info/People/kozen/kozen.html">Dexter Kozen</a>.
I also work closely with <!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><a href="http://www.cs.cornell.edu/Info/People/jyh/jyh.html">Jason
Hickey</a>.
<p>

<h3><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><a href="http://www.cs.cornell.edu/Info/People/crary/papers.html">Selected papers</a></h3>

<h3>Other Links</h3>
<ul>
<li>Mark Leone maintains a collection of
<!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><a href="http://www.cs.cmu.edu/afs/cs.cmu.edu/user/mleone/web/language-research.html">
programming language research resources</a>.

<li>You can
<!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><a href="http://cs-tr.cs.cornell.edu">search computer science technical reports</a> online.

<li><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><a href="http://www.lassp.cornell.edu/ardlouis/Christian/GRADLIFE/GradIVL.html">Cornell Grad Life Bible
Studies home page</a>

<li><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><a href="http://www.hyperion.com/lurk">The Lurker's Guide to Babylon 5</a>.
</ul>

<hr>

<blockquote>
"Of all the commandments, which is the most important?"<p>

"The most important one," answered Jesus, "is this: 'Hear, O Israel, the
Lord our God, the Lord is one.  Love the Lord your God with all your heart and
with all your soul and with all your mind and with all your strength.' The
second is this: 'Love your neighbor as yourself.'  There is no commandment
greater than these."<p>
-- Mark 12:29-31
</blockquote>
<hr>
<!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><a href="http://www.info.cornell.edu/CUHomePage.html">Cornell University home page</a><br>
<!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><a href="http://www.cs.cornell.edu">Department of Computer Science home page</a>