<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div class="elementToProof" style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
Hi all,</div>
<div class="elementToProof" style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div class="elementToProof" style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
as my PhD finally approaches to the end, I have put together the mechanizations in Agda that I have done during my study, where I focus on normalization proofs of different type theories:
<a href="https://hustmphrrr.github.io/mech-type-theories/" id="LPlnk397212">https://hustmphrrr.github.io/mech-type-theories/</a></div>
<div class="elementToProof" style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div class="elementToProof" style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
A list of type theories are available here: <a href="https://hustmphrrr.github.io/mech-type-theories/README.html" id="LPlnk567669">
https://hustmphrrr.github.io/mech-type-theories/README.html</a></div>
<div class="elementToProof" style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div class="elementToProof" style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
The library contains many type theories, including STLC, MLTT and also my own work. In this library, I implemented different normalization proofs, including presheaf models and untyped domain models based on Andreas' habilitation thesis. It is quite notable
that the NbE proof in this library is very concise; it has only 8k LoC and can be shrunk a bit further. I think this is quite amazing, as usually we don't really think that Agda can compress LoC that much compared to, e.g. Coq, proof assistants that come with
powerful proof automations. I think the concision of the library not only provides research value, but also should be helpful for educational purposes. I also believe this library provides an alternative to other mechanizations out there for people to base
their work on. So please do not hesitate and take a quick look!</div>
<div class="elementToProof" style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div class="elementToProof" style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
Since it is very unlikely for me to work on type theory substantially after graduation, at least not full-time, I will probably only spend the minimal effort to make sure that the library catches up with the latest Agda and stdlib. I would like to welcome people
to contribute and/or use this library for anything. </div>
<div class="elementToProof" style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div class="elementToProof" style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
Any other suggestions are also welcomed. I will try to address as much as possible before the winter comes.</div>
<div class="elementToProof" style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="Signature">
<div style="font-size:12pt;color:#000000;font-family:Calibri,Arial,Helvetica,sans-serif" dir="ltr" id="divtagdefaultwrapper">
<span style="font-size: 16px;"><b>Thanks,</b></span></div>
<div style="direction: ltr; font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 16px; color: rgb(0, 0, 0);">
<b>Jason Hu</b></div>
<div style="direction: ltr; font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<span style="font-size: 16px;"><b><a href="https://hustmphrrr.github.io/">https://hustmphrrr.github.io/</a></b></span><br>
</div>
</div>
</body>
</html>