Child pages
  • Yoshiki Kinoshita's second visit to Bath

Versions Compared


  • This line was added.
  • This line was removed.
  • Formatting was changed.
Comment: Migrated to Confluence 4.0


Wessex Theory Seminar, 14 Apr.
I gave a talk with the title ¿Hoare Hoare in Agda.¿ I encoded or implemented Hoare Logic in Agda with Makoto Takeyama. My talk is about design decisions I made during this work. Slides are included as Appendix A in this report.