408indexindex.xmlSteven SchaeferSteven SchaeferfalseI am a third-year PhD student at the University of Michigan. I am advised by Max New and Jean-Baptiste Jeannin.I am interested in the mathematical study of programming languages. In particular, I study the application of logic and category theory to the design and implementation of provably correct software.246sss-000Fsss-000F.xmlResearch Interests202486Steven Schaefer235sss-000Jsss-000J.xmlFormal Grammars as Types2024812Steven SchaeferAn ordered, linear type theory can serve as an appropriate foundation for the design and implementation of intrinsically verified parsers.Such a calculus expresses the mathematical specification of a parser simultaneously with its implementation. For this reason, parsers that type check internal to the theory are correct-by-construction.237sss-000Ksss-000K.xmlMechanized Category Theory2024812Contribution to a lab-wide effort formalizing category theoretical proofs in Cubical Agda.248sss-000Gsss-000G.xmlTeaching202486Steven SchaeferGSI for EECS 483 Compiler Construction250notesnotes.xmlNotesSteven SchaeferHere are links to some of my ongoing forest of notesCategorial Grammar252linkslinks.xmlLinksSteven SchaeferGitHub
Mastodon
LinkedIn254sss-000Esss-000E.xmlAbout This Website202486Steven SchaeferI built this website using Forester. I aim to frequently add notes to my forest, so this site is perpetually a work-in-progress.You may search through this site using Ctrl-k/Cmd-k.Related410jeanbaptistejeanninjeanbaptistejeannin.xmlJean-Baptiste Jeanninhttps://public.websites.umich.edu/~jeannin/Professor411maxsnewmaxsnew.xmlMax S. NewPersonhttps://maxsnew.com/Assistant Professor