References

1. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich & Steve Zdancewic (2005): Mechanized Metatheory for the Masses: The PoplMark Challenge. In: TPHOLs, LNCS 3603. Springer, pp. 50–65, doi:10.1007/11541868_4.
2. Yves Bertot, G[Pleaseinsert\PrerenderUnicodeéintopreamble]rard Huet, Jean-Jacques L[Pleaseinsert\PrerenderUnicodeéintopreamble]vy & Gordon Plotkin (2009): Theorem proving support in programming language semantics, chapter 15, pp. 337–361. Cambridge University Press. Available at http://hal.inria.fr/inria-00160309/.
3. Fabricio Chalub & Christiano Braga (2007): Maude MSOS Tool. ENTCS 176(4), pp. 133–146, doi:10.1016/j.entcs.2007.06.012.
4. Adam Chlipala (2011): Certified Programming with Dependent Types. Available at http://adam.chlipala.net/cpdt/. To appear.
5. Benjamin Delaware, William R. Cook & Don Batory (2011): Modular Mechanized Metatheory. In preparation.
6. Chung-Kil Hur (2010): Heq: A Coq Library for Heterogeneous Equality. Available at http://www.pps.jussieu.fr/~gil/Heq/. Informal presentation at the 2nd Coq Workshop.
7. Peter D. Mosses (2004): Modular Structural Operational Semantics. J. of Logic and Algebraic Programming 60-61, pp. 195–228, doi:10.1016/j.jlap.2004.03.008.
8. Peter D. Mosses (2005): A Constructive Approach to Language Definition. J. of Universal Computer Science 11(7), pp. 1117–1134, doi:10.3217/jucs-011-07-1117.
9. Peter D. Mosses (2009): Component-Based Semantics. In: Proc. of SAVCBS'09. ACM Press, pp. 3–10, doi:10.1145/1596486.1596489.
10. Peter D. Mosses & Mark J. New (2009): Implicit Propagation in Structural Operational Semantics. ENTCS 229(4), pp. 49–66, doi:10.1016/j.entcs.2009.07.073.
11. Scott Owens (2008): A Sound Semantics for OCaml light. In: Proc. of ESOP'08, LNCS 4960. Springer, pp. 1–15, doi:10.1007/978-3-540-78739-6_1.
12. Gordon D. Plotkin (2004): A Structural Approach to Operational Semantics. J. of Logic and Algebraic Programming 60-61, pp. 17–139.
13. Matthieu Sozeau & Nicolas Oury (2008): First-Class Type Classes. In: TPHOLs, LNCS 5170. Springer, pp. 278–293, doi:10.1007/978-3-540-71067-7_23.
14. Bas Spitters & Eelis van der Weegen (2011): Type Classes for Mathematics in Type Theory. MSCS 21, pp. 1–31, doi:10.1017/S0960129511000119.
15. The Coq Development Team (2010): The Coq Proof Assistant Reference Manual – Version V8.3. Available at http://coq.inria.fr.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org