[Agda] Verifying type inference in Agda?

[Philip Wadler]

See
    https://plfa.github.io/Inference/
which provides a textbook account of bidirectional inference for STLC. Go
well, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/



On Tue, 29 Sep 2020 at 22:40, William Harrison <
william.lawrence.harrison at gmail.com> wrote:

> Hi,
>
> I’m wondering if anyone has a pointer to a case study of verifying a type
> inference algorithm in Agda? Simple examples (even a toy example) would be
> alright (even preferred). I’m mainly interested in the structuring of the
> verifications in Agda.
>
> Thanks,
> Bill
>
> Sent from my iPad
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200930/503c7275/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200930/503c7275/attachment.ksh>