Congratulations Mario!
I would also have liked to attend, but the timing was very bad for me (1AM in my timezone) and I'm a bit busy currently. I'd like to ask "What is your next step now?", but I guess this is already answered somewhere in the slides, towards the end! On 14/06/2022 18:55, Mario Carneiro wrote:
Thanks everyone for the well wishes. Everything went well and I'm a doctor now. The slides for the talk are up at https://digama0.github.io/mm0/thesis-slides.pdf , and I might record a version of the talk for youtube at some point. On Tue, Jun 14, 2022 at 3:21 AM heiphohmia via Metamath <[email protected]> wrote: Congrats, Mario, on making it through a Ph.D. thesis defense! Hope you destroyed the grilling. I would love to have attended, but it was in the middle of the night in my time zone. Will a recording be available as well? Jon P <[email protected]> wrote: > Hey Mario, I've been enjoying your thesis and just wanted to wish you luck > with your defence today :) > > On Wednesday, June 8, 2022 at 4:49:28 AM UTC+1 [email protected] wrote: > > > To clarify, that is Mon, Jun 13 2022, 1:00 PM EDT > > > > On Tue, Jun 7, 2022 at 11:45 PM Mario Carneiro <[email protected]> wrote: > > > >> My dissertation defense on Metamath Zero will be held next week! It's > >> open to the public. > >> > >> Please join us for the Final Public Oral Examination for the degree, > >> Doctor of Philosophy in Pure and Applied Logic > >> > >> Mario Carneiro > >> > >> Title: Metamath Zero: From Logic, to Proof Assistant, to Verified Compiler > >> > >> Committee: > >> Jeremy Avigad, Carnegie Mellon University, chair > >> Thomas Hales, University of Pittsburgh > >> Wilfried Sieg, Carnegie Mellon University > >> John Harrison, Amazon Web Services > >> > >> Date & time: Mon, Jun 13 2022, 1:00 PM (45 minutes talk + questions) > >> Location: (Baker Hall 150 or) Zoom: > >> https://cmu.zoom.us/j/98691564266?pwd=R0ZSSk9qSS9QY3N5WnRLakJWcDJ4UT09 > >> > >> Thesis: https://digama0.github.io/mm0/thesis.pdf > >> > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected] <mailto:metamath%[email protected]>. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/62a83700.1c69fb81.8e039.badbSMTPIN_ADDED_BROKEN%40gmr-mx.google.com. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuvcz7ubMAAhwhN-WKLL%2BwgoTZQqMcSqy3dESy-uw3jNA%40mail.gmail.com <https://groups.google.com/d/msgid/metamath/CAFXXJSuvcz7ubMAAhwhN-WKLL%2BwgoTZQqMcSqy3dESy-uw3jNA%40mail.gmail.com?utm_medium=email&utm_source=footer>.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3004db09-176b-1dad-17ab-94da17988679%40gmx.net.
