@article(Alpuente:2014:MOE:2608865.2609198,
 author       = {Mar\'{\i}a Alpuente and Santiago Escobar and Javier Espert and Jos{\'e} Meseguer},
 year         = {2014},
 title        = {A Modular Order-sorted Equational Generalization Algorithm},
 journal      = {Inf. Comput.},
 volume       = {235},
 pages        = {98--136},
 doi          = {10.1016/j.ic.2014.01.006},
)
@article(BEIERLE1994123,
 author       = {Christoph Beierle and Gregor Meyer},
 year         = {1994},
 title        = {Run-time type computations in the Warren Abstract machine},
 journal      = {The Journal of Logic Programming},
 volume       = {18},
 number       = {2},
 pages        = {123 -- 148},
 doi          = {10.1016/0743-1066(94)90049-3},
 url          = {http://www.sciencedirect.com/science/article/pii/0743106694900493},
)
@inproceedings(bogdanas-rosu-2015-popl,
 author       = {Bogd\u{a}na\c{s}, Denis and Ro\c{s}u, Grigore},
 year         = {2015},
 title        = {{K-Java: A Complete Semantics of Java}},
 booktitle    = {Proceedings of the 42nd Symposium on Principles of Programming Languages (POPL'15)},
 publisher    = {ACM},
 pages        = {445--456},
 doi          = {10.1145/2676726.2676982},
)
@inproceedings(clavel00principles,
 author       = {Manuel Clavel and Steven Eker and Patrick Lincoln and Jos{\'e} Meseguer},
 year         = {1996},
 title        = {Principles of Maude},
 editor       = {J. Meseguer},
 booktitle    = {Electronic Notes in Theoretical Computer Science},
 volume       = {4},
 publisher    = {Elsevier Science Publishers},
 doi          = {10.1016/S1571-0661(04)00034-9},
)
@inbook(Comon1990,
 author       = {Hubert Comon},
 year         = {1990},
 title        = {Equational formulas in order-sorted algebras},
 pages        = {674--688},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/BFb0032066},
)
@inbook(Corbineau2008,
 author       = {Pierre Corbineau},
 year         = {2008},
 title        = {A Declarative Language for the Coq Proof Assistant},
 pages        = {69--84},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/978-3-540-68103-8_5},
)
@inproceedings(eker-etal-02wrla,
 author       = {Steven Eker and Merrill Knapp and Keith Laderoute and Patrick Lincoln and Carolyn Talcott},
 year         = {2002},
 title        = {Pathway Logic: Executable Models of Biological Networks},
 booktitle    = {Fourth International Workshop on Rewriting Logic and Its Applications (WRLA 2002), Pisa, Italy, September 19 --- 21, 2002},
 series       = {Electronic Notes in Theoretical Computer Science},
 volume       = {71},
 publisher    = {Elsevier},
 doi          = {10.1016/S1571-0661(05)82533-2},
)
@inproceedings(EMSltl2002,
 author       = {Steven Eker and Jos{\'e} Meseguer and Ambarish Sridharanarayanan},
 year         = {2003},
 title        = {The Maude LTL Model Checker and Its Implementation},
 booktitle    = {Proceedings of the 10th International Conference on Model Checking Software},
 series       = {SPIN'03},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 pages        = {230--234},
 doi          = {10.1007/3-540-44829-2_16},
)
@inproceedings(ellison-rosu-2012-popl,
 author       = {Chucky Ellison and Grigore Rosu},
 year         = {2012},
 title        = {An Executable Formal Semantics of C with Applications},
 booktitle    = {Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12)},
 publisher    = {ACM},
 pages        = {533--544},
 doi          = {10.1145/2103656.2103719},
)
@inbook(Filaretti2014,
 author       = {Daniele Filaretti and Sergio Maffeis},
 year         = {2014},
 title        = {An Executable Formal Semantics of PHP},
 pages        = {567--592},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/978-3-662-44202-9_23},
)
@inproceedings(Goguen:1985:OSO:646239.683375,
 author       = {Joseph A. Goguen and Jean-Pierre Jouannaud and Jos{\'e} Meseguer},
 year         = {1985},
 title        = {Operational Semantics for Order-Sorted Algebra},
 booktitle    = {Proceedings of the 12th Colloquium on Automata, Languages and Programming},
 publisher    = {Springer-Verlag},
 address      = {London, UK, UK},
 pages        = {221--231},
 doi          = {10.1007/BFb0015747},
)
@article(Goguen:1992:OAI:146982.146984,
 author       = {Joseph A. Goguen and Jos{\'e} Meseguer},
 year         = {1992},
 title        = {Order-sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations},
 journal      = {Theor. Comput. Sci.},
 volume       = {105},
 number       = {2},
 pages        = {217--273},
 doi          = {10.1016/0304-3975(92)90302-V},
)
@inproceedings(hathhorn-ellison-rosu-2015-pldi,
 author       = {Chris Hathhorn and Chucky Ellison and Ro\c{s}u, Grigore},
 year         = {2015},
 title        = {Defining the Undefinedness of C},
 booktitle    = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15)},
 publisher    = {ACM},
 pages        = {336--345},
 doi          = {10.1145/2813885.2737979},
)
@inbook(Kirchner1988,
 author       = {Claude Kirchner and H{\'e}l{\`e}ne Kirchner and Jos{\'e} Meseguer},
 year         = {1988},
 title        = {Operational semantics of OBJ-3},
 pages        = {287--301},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/3-540-19488-6_123},
)
@(llvmsemantics,
 author       = {Liyi Li and Elsa Gunter},
 year         = {2016},
 title        = {LLVM Semantics},
 url          = {https://github.com/kframework/llvm-semantics},
)
@inbook(martioliet00rewriting,
 author       = {Mart{\'i}-Oliet, Narciso and Jos{\'e} Meseguer},
 year         = {2002},
 title        = {Rewriting Logic as a Logical and Semantic Framework},
 pages        = {1--87},
 publisher    = {Springer Netherlands},
 address      = {Dordrecht},
 doi          = {10.1007/978-94-017-0464-9_1},
)
@article(MARTIOLIET2002121,
 author       = {Mart{\'i}-Oliet, Narciso and Jos{\'e} Meseguer},
 year         = {2002},
 title        = {Rewriting logic: roadmap and bibliography},
 journal      = {Theoretical Computer Science},
 volume       = {285},
 number       = {2},
 pages        = {121 -- 154},
 doi          = {10.1016/S0304-3975(01)00357-7},
 url          = {http://www.sciencedirect.com/science/article/pii/S0304397501003577},
 note         = {Rewriting Logic and its Applications},
)
@inproceedings(jose111,
 author       = {Jos{\'e} Meseguer},
 year         = {1999},
 title        = {Research Directions in Rewriting Logic},
 editor       = {Ulrich Berger and Helmut Schwichtenberg},
 booktitle    = {Computational Logic},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {347--398},
 doi          = {10.1007/978-3-642-58622-4_10},
)
@article(Mspecverrwl2003,
 author       = {Jos{\'e} Meseguer},
 year         = {2003},
 title        = {Software specification and verification in rewriting logic},
 journal      = {NATO SCIENCE SERIES SUB SERIES III COMPUTER AND SYSTEMS SCIENCES},
 volume       = {191},
 pages        = {133--194},
)
@article(Meseguer:1989:OU:75739.75743,
 author       = {Jos{\'e} Meseguer and Joseph A. Goguen and Gert Smolka},
 year         = {1989},
 title        = {Order-sorted Unification},
 journal      = {J. Symb. Comput.},
 volume       = {8},
 number       = {4},
 pages        = {383--413},
 doi          = {10.1016/S0747-7171(89)80036-7},
)
@article(Meseguer2017,
 author       = {Jos{\'e} Meseguer and Stephen Skeirik},
 year         = {2017},
 title        = {Equational formulas and pattern operations in initial order-sorted algebras},
 journal      = {Formal Aspects of Computing},
 volume       = {29},
 number       = {3},
 pages        = {423--452},
 doi          = {10.1007/s00165-017-0415-5},
)
@book(Milner:1997:DSM:549659,
 author       = {Robin Milner and Mads Tofte and David Macqueen},
 year         = {1997},
 title        = {The Definition of Standard ML},
 publisher    = {MIT Press},
 address      = {Cambridge, MA, USA},
)
@inproceedings(park-stefanescu-rosu-2015-pldi,
 author       = {Daejun Park and \c{S}tef\u{a}nescu, Andrei and Ro\c{s}u, Grigore},
 year         = {2015},
 title        = {{KJS}: A Complete Formal Semantics of {JavaScript}},
 booktitle    = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15)},
 publisher    = {ACM},
 pages        = {346--356},
 doi          = {10.1145/2737924.2737991},
)
@incollection(isabelle,
 author       = {Lawrence C. Paulson},
 year         = {1990},
 title        = {{Isabelle}: The Next 700 Theorem Provers},
 editor       = {P. Odifreddi},
 booktitle    = {Logic and Computer Science},
 publisher    = {Academic Press},
 pages        = {361--386},
)
@article(rosu-serbanuta-2010-jlap,
 author       = {Ro{\c s}u, Grigore and {\c S}erb{\u a}nu{\c t}{\u a}, Traian Florin},
 year         = {2010},
 title        = {An Overview of the {K} Semantic Framework},
 journal      = {Journal of Logic and Algebraic Programming},
 volume       = {79},
 number       = {6},
 pages        = {397--434},
 doi          = {10.1016/j.jlap.2010.03.012},
)
@inproceedings(Stell:2002:FOA:646061.676166,
 author       = {John G. Stell},
 year         = {2002},
 title        = {A Framework for Order-Sorted Algebra},
 booktitle    = {Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology},
 series       = {AMAST '02},
 publisher    = {Springer-Verlag},
 address      = {London, UK, UK},
 pages        = {396--410},
 doi          = {10.1007/3-540-45719-4_27},
)
@inproceedings(fdr,
 author       = {Alexandre Boulgakov A.W. Roscoe Thomas Gibson-Robinson, Philip Armstrong},
 year         = {2014},
 title        = {{FDR3 --- A Modern Refinement Checker for CSP}},
 editor       = {Erika \'{A}brah\'{a}m and Klaus Havelund},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {8413},
 pages        = {187--201},
 doi          = {10.1007/978-3-642-54862-8_13},
)
@article(wang1952,
 author       = {Hao Wang},
 year         = {1952},
 title        = {Logic of many-sorted theories},
 journal      = {Journal of Symbolic Logic},
 volume       = {17},
 number       = {2},
 pages        = {105--116},
 doi          = {10.2307/2266241},
)