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.
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/.
Adam Chlipala (2011):
Certified Programming with Dependent Types.
Available at http://adam.chlipala.net/cpdt/.
To appear.
Benjamin Delaware, William R. Cook & Don Batory (2011):
Modular Mechanized Metatheory.
In preparation.
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.
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.
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.
Peter D. Mosses (2009):
Component-Based Semantics.
In: Proc. of SAVCBS'09.
ACM Press,
pp. 3–10,
doi:10.1145/1596486.1596489.
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.
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.
Gordon D. Plotkin (2004):
A Structural Approach to Operational Semantics.
J. of Logic and Algebraic Programming 60-61,
pp. 17–139.
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.
Bas Spitters & Eelis van der Weegen (2011):
Type Classes for Mathematics in Type Theory.
MSCS 21,
pp. 1–31,
doi:10.1017/S0960129511000119.
The Coq Development Team (2010):
The Coq Proof Assistant Reference Manual – Version V8.3.
Available at http://coq.inria.fr.