Add stubs for related work

Author: jacobmischka

src/proof-assistants.bib

@@ -19,42 +19,6 @@ @article{abel2001human
 	year = {2001}
 }
 
-@article{JSCert,
-	author = {Bodin, Martin and Chargueraud, Arthur and Filaretti, Daniele and Gardner, Philippa and Maffeis, Sergio and Naudziuniene, Daiva and Schmitt, Alan and Smith, Gareth},
-	title = {A Trusted Mechanised JavaScript Specification},
-	year = {2014},
-	issue_date = {January 2014},
-	publisher = {Association for Computing Machinery},
-	address = {New York, NY, USA},
-	volume = {49},
-	number = {1},
-	issn = {0362-1340},
-	url = {https://doi.org/10.1145/2578855.2535876},
-	doi = {10.1145/2578855.2535876},
-	journal = {SIGPLAN Not.},
-	month = jan,
-	pages = {87–100},
-	numpages = {14},
-	keywords = {mechanised semantics, coq, javascript}
-}
-
-@inproceedings{JSCertInp,
-	author = {Bodin, Martin and Chargueraud, Arthur and Filaretti, Daniele and Gardner, Philippa and Maffeis, Sergio and Naudziuniene, Daiva and Schmitt, Alan and Smith, Gareth},
-	title = {A Trusted Mechanised JavaScript Specification},
-	year = {2014},
-	isbn = {9781450325448},
-	publisher = {Association for Computing Machinery},
-	address = {New York, NY, USA},
-	url = {https://doi.org/10.1145/2535838.2535876},
-	doi = {10.1145/2535838.2535876},
-	booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
-	pages = {87–100},
-	numpages = {14},
-	keywords = {mechanised semantics, javascript, coq},
-	location = {San Diego, California, USA},
-	series = {POPL ’14}
-}
-
 @inproceedings{SASyLF,
 	author = {Aldrich, Jonathan and Simmons, Robert J. and Shin, Key},
 	title = {SASyLF: An Educational Proof Assistant for Language Theory},

src/thesis.bib

@@ -1,3 +1,11 @@
+@online{WasmIsabelle,
+	author = {Mischka, Jacob and Watt, Conrad},
+	year = {2020},
+	date = {2020-05-17},
+	url = {https://github.com/jacobmischka/wasm-isabelle},
+	urldate = {2020-07-14}
+}
+
 @inproceedings{WattMechanizing,
 	author = {Watt, Conrad},
 	title = {Mechanising and Verifying the WebAssembly Specification},
@@ -377,3 +385,50 @@ @online{FlashSecurityUpdates
 	url = {https://helpx.adobe.com/security/products/flash-player.html},
 	urldate = {2020-07-14}
 }
+
+@report{WasmCoqMechanization,
+	title = {A Mechanized Formalization of the WebAssembly Specification in Coq},
+	author = {Xuan Huang},
+	publisher = {Rochester Institute of Technology},
+	address = {Rochester, NY 14586},
+	year = {2019},
+	url = {https://www.cs.rit.edu/~mtf/student-resources/20191_huang_mscourse.pdf},
+	urldate = {2020-07-14}
+}
+
+@article{JSCert,
+	author = {Bodin, Martin and Chargueraud, Arthur and Filaretti, Daniele and Gardner, Philippa and Maffeis, Sergio and Naudziuniene, Daiva and Schmitt, Alan and Smith, Gareth},
+	title = {A Trusted Mechanised JavaScript Specification},
+	year = {2014},
+	issue_date = {January 2014},
+	publisher = {Association for Computing Machinery},
+	address = {New York, NY, USA},
+	volume = {49},
+	number = {1},
+	issn = {0362-1340},
+	url = {https://doi.org/10.1145/2578855.2535876},
+	doi = {10.1145/2578855.2535876},
+	journal = {SIGPLAN Not.},
+	month = jan,
+	pages = {87–100},
+	numpages = {14},
+	keywords = {mechanised semantics, coq, javascript}
+}
+
+@inproceedings{JSCertInp,
+	author = {Bodin, Martin and Chargueraud, Arthur and Filaretti, Daniele and Gardner, Philippa and Maffeis, Sergio and Naudziuniene, Daiva and Schmitt, Alan and Smith, Gareth},
+	title = {A Trusted Mechanised JavaScript Specification},
+	year = {2014},
+	isbn = {9781450325448},
+	publisher = {Association for Computing Machinery},
+	address = {New York, NY, USA},
+	url = {https://doi.org/10.1145/2535838.2535876},
+	doi = {10.1145/2535838.2535876},
+	booktitle = {Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+	pages = {87–100},
+	numpages = {14},
+	keywords = {mechanised semantics, javascript, coq},
+	location = {San Diego, California, USA},
+	series = {POPL ’14}
+}
+

src/thesis.tex

@@ -577,6 +577,7 @@ \chapter{Incremental Soundness}
 and Tail Call\cite{TailCallProposal}.
 Definitions and proofs for the type checker and interpreter are also updated
 accordingly.
+The source code for my mechanization can be found on GitHub\cite{WasmIsabelle}.
 
 A great deal of the challenge in this task involved learning how to effectively
 use Isabelle at the same time.
@@ -871,6 +872,26 @@ \section{Tail Call}
 
 \chapter{Related Work} % TODO
 
+\citeauthor{WasmCoqMechanization} developed an independent mechanization of
+WebAssembly using the Coq proof assistant, and came close to proving its
+soundness\cite{WasmCoqMechanization}.
+
+\citeauthor{JSCert} mechanized the JavaScript ECMAScript 5 standard in
+Coq, and created a reference interpreter proved correct with respect to
+the mechanization.
+
+\citeauthor{RustBelt} mechanized a core calculus of the Rust programming
+language using the Iris proof assistant\cite{RustBelt}.
+Rust is a modern systems language and one of the leading languages with
+support for compiling to WebAssembly.
+\citeauthor{RustBeltRelaxed} extended this work, accounting for relaxed-memory
+operations in use by concurrent Rust programs\cite{RustBeltRelaxed}.
+
+\citeauthor{Watt_2020}, the author of the original Isabelle WebAssembly
+mechanization on which my work is based, has mechanized the JavaScript memory
+model in Coq, finding errors in JavaScript's specification causing concurrency
+issues and compilation problems\cite{Watt_2020}.
+
 \chapter{Future Work} % TODO
 
 Certainly, much remains to be done in the area of WebAssembly soundness
@@ -891,9 +912,8 @@ \chapter{Future Work} % TODO
 Reference Types Proposal\cite{ReferenceTypesProposalOverview,WeakeningWasm}
 and phase 2 Threading Proposal\cite{ThreadingProposalOverview,WeakeningWasm}.
 
-\chapter{Conclusion} % TODO
+\chapter{Conclusion}
 
-% One paragraph summarizing what I did
 This paper investigates the WebAssembly language and the soundness of its
 type system.
 Beginning with an existing mechanized proof of the core language using the
@@ -905,7 +925,30 @@ \chapter{Conclusion} % TODO
 \citeauthor{WattMechanizing}, and plans are in place to integrate the changes
 into the official source.
 
-% TODO: Another paragraph summarizing what I learned (what's the point?)
+Over the course of this project I have had the opportunity to join the
+WebAssembly community, learn about the language and its origins, and take
+part in Community Group and subgroup video conference meetings.
+Gaining understanding of a core standardized language for the Web during its
+infancy and becoming familiar with its evolution process will be of immense
+benefit to me as a web developer as the language and ecosystem matures.
+On a higher level, my efforts in understanding and modeling a language
+specification and its type system and proving its soundness has given me a
+deeper understanding of programming language design and type theory as a whole.
+Small details in an instruction's execution or typing rules often have large
+implications when the program is checked or executed.
+Even for a rather simple language like WebAssembly with its four primitive
+types, small instruction set, and straightforward memory and execution models,
+issues can quickly arise and soundness is lost if a language feature is modeled
+even slightly incorrectly---for example when asserting that an incorrect number
+of values are present.
+Ensuring soundness and proper execution is critical when designing a language
+so that it holds the properties that it claims to: the type system will prevent
+bugs and the language will do what the programmer tells it to.
+Despite the importance of this assurance, it is challenging to do so, and
+particularly difficult to ensure that it stays so when making changes to the
+language.
+Proof mechanization is one way to ease this burden, providing language
+authors a more foolproof way to keep their promises to their users.
 
 % \appendix