Curry-Howard correspondence describes a language that corresponds to propositional logic. Since modal logic is an extension of propositional logic, then what language corresponds to modal logic? If there is one, then what is it good for? Murphy's dissertation argues that a programming language designed based on modal type systems can provide elegant abstractions to organize local resources on different computers. In this thesis, I limit his argument to simple web programming and claim that a modal logic based language provides a way to write readable code and correct web applications. To do this, I defined a minimal language called ML5 in the Agda proof assistant and then implemented a compiler to JavaScript for it and proved its static correctness. The compiler is a series of type directed translations through fully formalized languages, the last one of which is a very limited subset of JavaScript. As opposed to Murphy's compiler, this one compiles to JavaScript both on the front end and back end through Node.js. Currently the last step of conversion to JavaScript is not entirely complete. We have not specified the conversion rules for the modal types, and network communication only has a partially working proof-of-concept.
"},{"label":"Degree","value":["Bachelor of Arts with Departmental Honors"]},{"label":"Administrative Note","value":"2017