http://mw.hh.se/wg211/index.php?action=history&feed=atom&title=WG211%2FM7Weirich1WG211/M7Weirich1 - Revision history2026-04-05T21:09:34ZRevision history for this page on the wikiMediaWiki 1.43.5http://mw.hh.se/wg211/index.php?title=WG211/M7Weirich1&diff=257&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>Adventures in Dependently-Typed Metatheory</h1><br />
<h3>Stephanie Weirich with Limin Jia, Jianzhou Zhao, Vilhelm Sj"oberg</h3><br />
<br />
Work-in-progress report<br />
<br />
Dependent type systems allow users to include computations in<br />
types, thereby allowing arbitrary expression of program properties.<br />
Because types include computations, the type system of such<br />
language must include a definition of program equivalence. For example,<br />
the type checker might reduce computations to some normal form to<br />
determine if they are the same. However, there are many ways to define<br />
equivalence for programs, and if we change our mind about what<br />
sort of equivalence to use, we must do all of the metatheory of<br />
the dependently-typed language over. For example, some definitions<br />
of equivalence may choose to ignore computationally-irrelevant terms,<br />
others may or may not be decidable if the computation language<br />
includes non-termination.<br />
<br />
In this talk, I will report on initial progress to define a language<br />
where the definition of equivalence is held abstract. Instead, we seek<br />
to determine the properties of the equivalence relation that are<br />
necessary to show that the language is type sound.<br />
<br />
* [[Media:211-deptyp.pdf | 211-deptyp.pdf ]]: Slides<br />
<br />
==File Attachments== <br />
<br />
*[[Media:211-deptyp.pdf | 211-deptyp.pdf]]</div>Admin