http://mw.hh.se/wg211/index.php?action=history&feed=atom&title=WG211%2FM7StumpWG211/M7Stump - Revision history2026-04-05T22:42:56ZRevision history for this page on the wikiMediaWiki 1.43.5http://mw.hh.se/wg211/index.php?title=WG211/M7Stump&diff=251&oldid=prevAdmin: 1 revision2011-12-12T10:06:28Z<p>1 revision</p>
<p><b>New page</b></p><div>[[Category:WG211]]<br />
<br />
<br />
<h1>Purifying Natural Deduction Using Sequent Calculus</h1><br />
<h3>Aaron Stump</h3><br />
<br />
The Curry-Howard isomorphism has proved a very fruitful<br />
connection between programming languages and logic for the past 30<br />
years or so. Proofs in intuitionistic natural deduction are<br />
identified with terms in typed lambda calculus, and various notions of<br />
reduction and equivalence of terms can then be exchanged between the<br />
logical and computational views. The case of disjunction (sum types)<br />
and existentials has not worked out so cleanly, however, requiring<br />
so-called commuting conversions. In this talk, I show how to remove<br />
the difficulties for disjunctions and existentials, by introducing new<br />
lambda calculus terms. These terms arise from a new and more direct<br />
term assignment to proofs in sequent calculus. The result is a type<br />
system for which we can easily adapt Girard's reducibility candidates<br />
to show strong normalization, and for which notions of extensionality<br />
for sum types and existentials become natural to state and accomodate<br />
in our notions of term reduction and equivalence. Both these results<br />
have been problematic with the traditional terms for disjunctions and<br />
existentials.<br />
<br />
* [[Media:stump-wg09.pdf | stump-wg09.pdf ]]: Slides<br />
<br />
==File Attachments== <br />
<br />
*[[Media:stump-wg09.pdf | stump-wg09.pdf]]</div>Admin