@inproceedings(ayd05:poplmark,
 author       = "Brian E. Aydemir and Aaron Bohannon and Matthew Fairbairn and J. Nathan Foster and Benjamin C. Pierce and Peter Sewell and Dimitrios Vytiniotis and Geoffrey Washburn and Stephanie Weirich and Steve Zdancewic",
 year         = "2005",
 title        = "Mechanized Metatheory for the Masses: The {\textsc {{P}opl{M}ark}} Challenge",
 booktitle    = "TPHOLs",
 series       = "LNCS",
 volume       = "3603",
 publisher    = "Springer",
 pages        = "50--65",
 doi          = "10.1007/11541868\_4",
)
@inbook(Bertot09,
 editor       = "Yves Bertot and G\begingroup \let \relax \relax \endgroup [Pleaseinsert\PrerenderUnicode{é}intopreamble]rard Huet and Jean-Jacques L\begingroup \let \relax \relax \endgroup [Pleaseinsert\PrerenderUnicode{é}intopreamble]vy and Gordon Plotkin",
 year         = "2009",
 title        = "Theorem proving support in programming language semantics",
 chapter      = "15",
 pages        = "337--361",
 publisher    = "Cambridge University Press",
 url          = "http://hal.inria.fr/inria-00160309/",
)
@article(ChalubB07,
 author       = "Fabricio Chalub and Christiano Braga",
 year         = "2007",
 title        = "{Maude MSOS Tool}",
 journal      = "ENTCS",
 volume       = "176",
 number       = "4",
 pages        = "133--146",
 doi          = "10.1016/j.entcs.2007.06.012",
)
@unpublished(Chlipala,
 author       = "Adam Chlipala",
 year         = "2011",
 title        = "Certified Programming with Dependent Types",
 url          = "http://adam.chlipala.net/cpdt/",
 note         = "To appear",
)
@unpublished(Delaware,
 author       = "Benjamin Delaware and William R. Cook and Don Batory",
 year         = "2011",
 title        = "Modular Mechanized Metatheory",
 note         = "In preparation",
)
@unpublished(Hur10,
 author       = "Chung-Kil Hur",
 year         = "2010",
 title        = "Heq: A Coq Library for Heterogeneous Equality",
 url          = "http://www.pps.jussieu.fr/~gil/Heq/",
 note         = "Informal presentation at the 2nd Coq Workshop",
)
@article(Mosses04,
 author       = "Peter D. Mosses",
 year         = "2004",
 title        = "Modular Structural Operational Semantics",
 journal      = "J. of Logic and Algebraic Programming",
 volume       = "60-61",
 pages        = "195--228",
 doi          = "10.1016/j.jlap.2004.03.008",
)
@article(Mosses05,
 author       = "Peter D. Mosses",
 year         = "2005",
 title        = "A Constructive Approach to Language Definition",
 journal      = "J. of Universal Computer Science",
 volume       = "11",
 number       = "7",
 pages        = "1117--1134",
 doi          = "10.3217/jucs-011-07-1117",
)
@inproceedings(Mosses09,
 author       = "Peter D. Mosses",
 year         = "2009",
 title        = "Component-{B}ased Semantics",
 booktitle    = "Proc. of SAVCBS'09",
 publisher    = "ACM Press",
 pages        = "3--10",
 doi          = "10.1145/1596486.1596489",
)
@article(MossesN09,
 author       = "Peter D. Mosses and Mark J. New",
 year         = "2009",
 title        = "Implicit Propagation in Structural Operational Semantics",
 journal      = "ENTCS",
 volume       = "229",
 number       = "4",
 pages        = "49--66",
 doi          = "10.1016/j.entcs.2009.07.073",
)
@inproceedings(Owens08,
 author       = "Scott Owens",
 year         = "2008",
 title        = "A Sound Semantics for {O}{C}aml light",
 booktitle    = "Proc. of ESOP'08",
 series       = "LNCS",
 volume       = "4960",
 publisher    = "Springer",
 pages        = "1--15",
 doi          = "10.1007/978-3-540-78739-6\_1",
)
@article(Plotkin04a,
 author       = "Gordon D. Plotkin",
 year         = "2004",
 title        = "A Structural Approach to Operational Semantics",
 journal      = "J. of Logic and Algebraic Programming",
 volume       = "60-61",
 pages        = "17--139",
)
@inproceedings(SozeauO08,
 author       = "Matthieu Sozeau and Nicolas Oury",
 year         = "2008",
 title        = "First-Class Type Classes",
 booktitle    = "TPHOLs",
 series       = "LNCS",
 volume       = "5170",
 publisher    = "Springer",
 pages        = "278--293",
 doi          = "10.1007/978-3-540-71067-7\_23",
)
@article(SpittersW11,
 author       = "Bas Spitters and Eelis van der Weegen",
 year         = "2011",
 title        = "Type Classes for Mathematics in Type Theory",
 journal      = "MSCS",
 volume       = "21",
 pages        = "1--31",
 doi          = "10.1017/S0960129511000119",
)
@manual(CoqManualV83,
 author       = "{The {Coq} Development Team}",
 year         = "2010",
 title        = "{The Coq Proof Assistant Reference Manual -- Version V8.3}",
 url          = "http://coq.inria.fr",
)