%%% ACM Press -> ACM

@inproceedings{ridge-margetson-2005,
  author = {Tom Ridge and James Margetson},
  title     = {A Mechanically Verified, Sound and Complete Theorem Prover
               for First Order Logic},
  booktitle = {TPHOLs 2005},
  year      = {2005},
  pages     = {294--309},
  editor = {Joe Hurd and Thomas F. Melham},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {3603}
}

@inproceedings{DBLP:conf/cade/SmolkaB13,
  author    = {Steffen Juilf Smolka and
               Jasmin Christian Blanchette},
  title     = {Robust, Semi-Intelligible {I}sabelle Proofs from {ATP} Proofs},
  booktitle = {PxTP@CADE},
  year      = {2013},
  pages     = {117-132}
}

@inproceedings{DBLP:conf/ifip1-7/MeydenZ06,
  author    = {Ron van der Meyden and
               Chenyi Zhang},
  title     = {A Comparison of Semantic Models for Noninterference},
  booktitle = {Formal Aspects in Security and Trust},
  year      = {2006},
  pages     = {235-249}
}

@inproceedings{DBLP:conf/sp/WittboldJ90,
  author    = {J. Todd Wittbold and
               Dale M. Johnson},
  title     = {Information Flow in Nondeterministic Systems},
  booktitle = {IEEE Symposium on Security and Privacy},
  year      = {1990},
  pages     = {144-161}
}

@book{klein-et-al-afp,
  title = "The Archive of Formal Proofs",
  editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher = "\url{http://isa-afp.org/}"}

@incollection{berghofer-2007,
  title = "First-Order Logic According to {F}itting",
  author = "Stefan Berghofer",
  booktitle = "The Archive of Formal Proofs",
  editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher = "\url{http://isa-afp.org/entries/FOL-Fitting.shtml}",
  year = 2007}

@incollection{tabl-handbook,
  author    = {Reiner H{\"a}hnle},
  title     = {Tableaux and Related Methods},
  editor = "Alan Robinson and Andrei Voronkov",
  booktitle = "Handbook of Automated Reasoning",
  volume = "I",
  pages     = {100--178},
  publisher = "Elsevier",
  year = 2001}

@inproceedings{DBLP:conf/itp/Cock13,
  author    = {David Cock},
  title     = {Practical Probability: Applying p{GCL} to Lattice Scheduling},
  booktitle = {ITP},
  year      = {2013},
  pages     = {311-327}
}



@article{DBLP:journals/cacm/KleinAEHCDEEKNSTW10,
  author    = {Gerwin Klein and
               June Andronick and
               Kevin Elphinstone and
               Gernot Heiser and
               David Cock and
               Philip Derrin and
               Dhammika Elkaduwe and
               Kai Engelhardt and
               Rafal Kolanski and
               Michael Norrish and
               Thomas Sewell and
               Harvey Tuch and
               Simon Winwood},
  title     = {se{L4}: formal verification of an operating-system kernel},
  journal   = {Commun. ACM},
  volume    = {53},
  number    = {6},
  year      = {2010},
  pages     = {107-115}
}


@inproceedings{harrison-1998,
  author    = {John Harrison},
  title     = {Formalizing Basic First Order Model Theory},
  booktitle = {TPHOLs '98},
  year      = {1998},
  pages     = {153--170},
  editor    = {Jim Grundy and
               Malcolm C. Newey},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {1479}
}

@inproceedings{barthe-isabelle,
  author    = {Gilles Barthe and
               Leonor Prensa Nieto},
  title     = {Formally verifying information flow type systems for concurrent
               and thread systems},
  booktitle = {FMSE},
  year      = {2004},
  pages     = {13--22}
}

@article{DBLP:journals/cj/AkbarpourATH10,
  author    = {Behzad Akbarpour and
               Amr T. Abdel-Hamid and
               Sofi{\`e}ne Tahar and
               John Harrison},
  title     = {Verifying a Synthesized Implementation of {IEEE}-754 Floating-Point
               Exponential Function using {HOL}},
  journal   = {Comput. J.},
  volume    = {53},
  number    = {4},
  year      = {2010},
  pages     = {465-488}
}

@INPROCEEDINGS{Mccarthy63abasis,
    author = {John McCarthy},
    title = {A Basis for a Mathematical Theory of Computation},
    booktitle = {Computer Programming and Formal Systems},
    year = {1963},
    pages = {33--70},
    publisher = {North-Holland}
}

@inproceedings{DBLP:conf/cav/EsparzaLNNSS13,
  author    = {Javier Esparza and
               Peter Lammich and
               Ren{\'e} Neumann and
               Tobias Nipkow and
               Alexander Schimpf and
               Jan-Georg Smaus},
  title     = {A Fully Verified Executable {LTL} Model Checker},
  booktitle = {CAV},
  year      = {2013},
  pages     = {463-478}
}

@article{pav-guarded,
  author    = {Dusko Pavlovi\`{c}},
  title     = {Guarded induction on final coalgebras},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {11},
  year      = {1998},
  pages     = {140--157}
}

@article{har-for-TP,
  author    = {John Harrison},
  title     = {Formal Proof -- Theory and Practice},
  journal   = {Notices of the American Mathematical Society},
  volume    = {55},
  year      = {2008},
  pages     = {1395--1406}
}


%number = "0",
@article{rut-relators,
title = "Relators and Metric Bisimulations",
journal = "Electr.\ Notes Theor.\ Comput.\ Sci.",
volume = "11",
pages = "252--258",
year = "1998",
author = "J. J. M. M. Rutten"
}
%%% HACK: TYPESETTING:  (Extended Abstract)


@article{barr-terminalCoalg,
title = "Terminal coalgebras in well-founded set theory",
journal = "Theor.\ Comput.\ Sci.",
volume = "114",
number = "2",
pages = "299--315",
year = "1993",
author = "Michael Barr"
}

%%% TYPESETTING: Hack in title and journal to get proper quote placement (American English)
@article{barr-corrections,
 author = {Barr, Michael},
 title = {Additions and corrections to ``{T}erminal coalgebras in well-founded set theory{\color{white}.}''\kern-.7em},
 journal = {{\upshape\phantom{''}}Theor. Comput. Sci.},
 volume = {124},
 issue = {1},
 monthXXX = {February},
 year = {1994},
 pages = {189--192},
}

@book{manes-sem,
 author = {Manes, Ernest G. and Arbib, Michael A.},
 title = {Algebraic Approaches to Program Semantics},
 year = {1986},
 publisher = {Springer}
}

@article{Church-HOL,
    author = {Church, Alonzo},
    journal = {J. Symb.\ Logic},
    number = {2},
    pages = {56--68},
    title = {A Formulation of the Simple Theory of Types},
    volume = {5},
    year = {1940}
}

@inproceedings{darvas-NonintDynamicLogic,
  author    = {{\'A}d{\'a}m Darvas and
               Reiner H{\"a}hnle and
               David Sands},
  title     = {A Theorem Proving Approach to Analysis of Secure Information
               Flow},
  booktitle = {SPC},
  year      = {2005},
  pages     = {193--209}
}

@INPROCEEDINGS{ms9,
author={Russo, Alejandro and Sabelfeld, Andrei},
booktitle={IEEE Computer Security Foundations Workshop},
title={Securing interaction between threads and the scheduler},
year={2006},
pages={177--189}
}


@inproceedings{mccul-hookUp,
  author    = {Daryl McCullough},
  title     = {Specifications for Multi-Level Security and a Hook-Up Property},
  booktitle = {IEEE Symposium on Security and Privacy},
  year      = {1987},
}

@misc{isabelle-list,
title = "The {I}sabelle mailing list",
note = "\url{https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users}",
year = "2013"}


@unpublished{paramMailingList,
  author = "Joachim Breitner",
  title = "Parametricity as a poor man's dependent typing",
  note = "\url{https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-February/msg00094.html}"
}

@unpublished{modularTypeAgda,
  author = "Christopher Schwaab and Jeremy G. Siek",
  title = "Modular Type-Safety Proofs in {A}gda",
  note = "To appear in \emph{{PLPV} 2013}"
}

@inproceedings{smiVol-multiThr,
 author = {Smith, Geoffrey and Volpano, Dennis},
 title = {Secure information flow in a multi-threaded imperative language},
 booktitle = {POPL},
 year = {1998},
 pages = {355--364}
}

@INPROCEEDINGS{ms7,
    author = {Andrei Sabelfeld and David Sands},
    title = {Probabilistic Noninterference for Multi-threaded Programs},
    booktitle = {IEEE Computer Security Foundations Workshop},
    year = {1999},
    pages = {200--214}
}

@article{boudCast,
title = "Noninterference for concurrent programs and thread systems",
journal = "Theoretical Computer Science",
volume = "281",
number = "1-2",
pages = "109--130",
year = "2002",
author = "G\'{e}rard Boudol and Ilaria Castellani"
}

@INPROCEEDINGS{ms11,
author={Smith, Geoffrey},
booktitle={IEEE Computer Security Foundations Workshop}, 
title={Probabilistic noninterference through weak probabilistic bisimulation},
year={2003},
pages={3--13}
}

@inproceedings{boudImproved,
  author    = {G{\'e}rard Boudol},
  title     = {On Typing Information Flow},
  booktitle = {ICTAC},
  year      = {2005},
  pages     = {366--380}
}

@article{smith-ImprovedTypingsProb,
  author    = {Geoffrey Smith},
  title     = {Improved typings for probabilistic noninterference in a
               multi-threaded language},
  journal   = {Journal of Computer Security},
  volume    = {14},
  number    = {6},
  year      = {2006},
  pages     = {591--623},
  ee        = {http://iospress.metapress.com/openurl.asp?genre=article{\&}issn=0926-227X{\&}volume=14{\&}issue=6{\&}spage=591},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@phdthesis{mantel-thesis,
title = "A Uniform Framework for the Formal Specification and Verification of Information Flow Security",
author = "Heiko Mantel",
year = 2003,
school = "University of Saarbr{\"u}cken"}

@InProceedings{mantel-ass,
  author	= {Heiko Mantel and David Sands and Henning Sudbrock},
  title		= {Assumptions and Guarantees for Compositional
		  Noninterference},
  booktitle	= {Proceedings of the 24th IEEE Computer Security Foundations
		  Symposium},
  publisher	= {IEEE Computer Society},
  address	= {Cernay-la-Ville, France},
  year		= 2011,
  pages		= {218--232},
}

@inproceedings{bai-weak,
  author    = {Christel Baier and
               Holger Hermanns},
  title     = {Weak Bisimulation for Fully Probabilistic Processes},
  booktitle = {CAV},
  year      = {1997},
  pages     = {119--130},
  ee        = {https://doi.org/10.1007/3-540-63166-6_14},
  crossref  = {DBLP:conf/cav/1997},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/cav/1997,
  editor    = {Orna Grumberg},
  title     = {Computer Aided Verification, 9th International Conference,
               CAV '97, Haifa, Israel, June 22-25, 1997, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {1254},
  year      = {1997},
  isbn      = {3-540-63166-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{mantel-schedInd,
  author    = {Heiko Mantel and
               Henning Sudbrock},
  title     = {Flexible Scheduler-Independent Security},
  booktitle = {ESORICS},
  year      = {2010},
  pages     = {116--133}
}


@article{pop-relalg,
year={2005},
journal={Algebra Universalis},
volume={53},
number={1},
title={Many-valued relation algebras},
author={Popescu, Andrei},
pages={73-108}
}

@article{pop-relalg2, 
year={2007},
journal={Algebra Universalis},
volume={56},
number={2},
title={Some algebraic theory for many-valued relation algebras},
author={Popescu, Andrei},
pages={211-235}
}

@inproceedings{DBLP:conf/csfw/Mantel00,
  author    = {Heiko Mantel},
  title     = {Possibilistic Definitions of Security - An Assembly Kit},
  booktitle = {CSFW},
  year      = {2000},
  pages     = {185-199}
}

@inproceedings{DBLP:conf/sp/ZakinthinosL97,
  author    = {Aris Zakinthinos and
               E. Stewart Lee},
  title     = {A General Theory of Security Properties},
  booktitle = {IEEE Symposium on Security and Privacy},
  year      = {1997},
  pages     = {94-102}
}

@article{DBLP:journals/aml/GeorgescuP04,
  author    = {George Georgescu and
               Andrei Popescu},
  title     = {Non-dual fuzzy connections},
  journal   = {Arch. Math. Log.},
  volume    = {43},
  number    = {8},
  year      = {2004},
  pages     = {1009-1039}
}

@article{DBLP:journals/mlq/Popescu04,
  author    = {Andrei Popescu},
  title     = {A general approach to fuzzy concepts},
  journal   = {Math. Log. Q.},
  volume    = {50},
  number    = {3},
  year      = {2004},
  pages     = {265-280}
}

@article{DBLP:journals/tse/McLean96,
  author    = {John McLean},
  title     = {A General Theory of Composition for a Class of ``Possibilistic''
               Properties},
  journal   = {IEEE Trans. Software Eng.},
  volume    = {22},
  number    = {1},
  year      = {1996},
  pages     = {53-67}
}


@unpublished{mas-thesis,
title = "Abstract Non-Interference-An Abstract Interpretation-based Approach to Secure Information Flow",
author = "Isabella Mastroeni",
note = "PhD thesis, Univ. of Verona, 2005."}

@inproceedings{DBLP:conf/icalp/TannenS91,
  author    = {Val Tannen and
               Ramesh Subrahmanyam},
  title     = {Logical and Computational Aspects of Programming with Sets/Bags/Lists},
  booktitle = {ICALP},
  year      = {1991},
  pages     = {60-75}
}


@unpublished{schropp-thesis,
title = "Instantiating deeply embedded many-sorted theories into {HOL} types in {I}sabelle",
author = "Andreas Schropp",
note = "Master Thesis, Technische Universit{\"a}t M{\"u}nchen, 2012.
\url{http://home.in.tum.de/~schropp}"}



@unpublished{pop-thesis,
title = "Contributions to the theory of syntax with bindings and to process algebra",
author = "Andrei Popescu",
note = "Ph.D.\ Thesis, Univ. of Illinois, 2010.
\url{http://www4.in.tum.de/~popescua/thesis.pdf}"}


@unpublished{pop-scripts,
title = "\url{http://www4.in.tum.de/~popescua/Scripts.zip}",
author = "",
note = ""}

@inproceedings{aydemirPOPL08,
  author    = {Brian E. Aydemir and
               Arthur Chargu{\'e}raud and
               Benjamin C. Pierce and
               Randy Pollack and
               Stephanie Weirich},
  title     = {Engineering formal metatheory},
  booktitle = {POPL 2008},
  year      = {2008},
  pages     = {3--15}
}


@article{gai-rob,
title = "An Institution-Independent Proof of the {R}obinson Consistency Theorem",
author = "Daniel G{\u a}in\u{a} and Andrei Popescu",
journal = "Studia Logica",
volume = 85,
number = "1",
year = 2007,
pages = "41--73"}

@article{gai-tar,
title = "An Institution-Independent Generalization of {T}arski's Elementary Chain Theorem",
author = "Daniel G{\u a}in\u{a} and Andrei Popescu",
journal = "Journal of Logic and Computation",
volume = "16",
number = "6",
year = 2007,
pages = "713--735"}

@inproceedings{pop-beh,
  author    = {Andrei Popescu and
               Grigore Ro\c{s}u},
  title     = {Behavioral extensions of institutions},
  booktitle = {CALCO},
  year      = {2005},
  pages     = {331--347},
}

@inproceedings{pop-TGL-WADT,
  author    = {Andrei Popescu and
               Grigore Ro\c{s}u},
  title     = {Term-Generic Logic},
  booktitle = {WADT},
  year      = {2008},
  pages     = {290--307},
}

@unpublished{TGL-latestTR,
title = "Term-Generic Logic",
author = "Andrei Popescu and Grigore Ro{\c s}u",
note = "Technical Report UIUCDCS-R-2009-3027.  Department of Computer Science, University of Illinois
at Urbana-Champaign, 2009"}

@inproceedings{pop-nonintSch,
  author    = {Andrei Popescu and
               Johannes H{\"o}lzl and
               Tobias Nipkow},
  title     = {Noninterfering Schedulers - When Possibilistic Noninterference
               Implies Probabilistic Noninterference},
  booktitle = {CALCO},
  year      = {2013},
  pages     = {236-252}
}

@unpublished{pop-nonintSch-rep,
  author = "Andrei Popescu and
               Johannes H{\"o}lzl and
               Tobias Nipkow",
  title = "Noninterfering Schedulers - When Possibilistic Noninterference
               Implies Probabilistic Noninterference",
  note = "Technical Report, TU M{\"u}nchen, 2013. 
  Available at \url{http://mediatum.ub.tum.de/?id=1159789}"
}


@inproceedings{pop-CCSweak,
  author    = {Andrei Popescu},
  title     = {Weak Bisimilarity Coalgebraically},
  booktitle = {CALCO'09},
  year      = {2009},
  pages     = {157--172},
}


@inproceedings{gun-proper,
  author    = {Elsa L. Gunter and Christopher J. Osborn and Andrei Popescu},
  title     = {Theory Support for Weak {H}igher {O}rder {A}bstract {S}yntax in {I}sabelle/{HOL}},
  booktitle = {LFMTP},
  pages = "12--20",
  year      = {2009},
}

@inproceedings{pop-HOASOnFOAS,
  author    = {Andrei Popescu and Elsa L. Gunter and Christopher J. Osborn},
  title     = {Strong Normalization of {S}ystem {F} by {HOAS} on top of {FOAS}},
  booktitle = {LICS},
  pages = "31--40",
  year      = {2010}
}


@inproceedings{felty-capretta,
  author    = {Venanzio Capretta and
               Amy P. Felty},
  title     = {Combining de {B}ruijn Indices and Higher-Order Abstract Syntax
               in {C}oq},
  booktitle = {TYPES},
  year      = {2006},
  pages     = {63--77}
}



@unpublished{Coind-scripts,
title = "The {I}sabelle formalization of an incremental coniductive proof system",
author = "Andrei Popescu",
note = "Tech. Rep., Univ. of Illinois at Urbana-Champaign, 2010.
http://hdl.handle.net/2142/14857"}


@unpublished{HOASOnFOAS-scripts,
title = "{HOAS} on top of {FOAS} formalized in {I}sabelle/{HOL}",
author = "Andrei Popescu",
note = "Technical report http://hdl.handle.net/2142/15449.
Department of Computer Science, University of Illinois
at Urbana-Champaign, 2010"}

@inproceedings{pop-Coind,
  author    = {Andrei Popescu and
               Elsa L. Gunter},
  title     = {Incremental Pattern-Based Coinduction for Process Algebra
               and Its {I}sabelle Formalization},
  booktitle = {FOSSACS},
  year      = {2010},
  pages     = {109-127}
}

@unpublished{Coind-TR,
title = "Incremental pattern-based coinduction for process algebra and its {I}sabelle formalization",
author = "Andrei Popescu and Elsa Gunter",
note = "Technical report http://hdl.handle.net/2142/14858.
Department of Computer Science, University of Illinois
at Urbana-Champaign, 2010"}


@unpublished{piSem-TR,
title = "A Fully Abstract Coalgebraic Semantics for the pi-calculus Under Weak Bisimilarity",
author = "Andrei Popescu",
note = "Technical report http://hdl.handle.net/2142/11530.
Department of Computer Science, University of Illinois
at Urbana-Champaign, 2009"}






@article{gut-AlgSpec,
  author    = {John V. Guttag and
               James J. Horning},
  title     = {The Algebraic Specification of Abstract Data Types},
  journal   = {Acta Inf.},
  volume    = {10},
  year      = {1978},
  pages     = {27--52},
}



@inproceedings{circCALCO09tool,
  author    = {Dorel Lucanu and
               Eugen-Ioan Goriac and
               Georgiana Caltais and
               Grigore Ro\c{s}u},
  title     = {{CIRC}: A Behavioral Verification Tool Based on Circular Coinduction},
  booktitle = {CALCO'09},
  year      = {2009},
  pages     = {433--442},
}


@inproceedings{alt-SNSystemFLego,
  author    = {Thorsten Altenkirch},
  title     = {A Formalization of the Strong Normalization Proof for {S}ystem
               {F} in {LEGO}},
  booktitle = {TLCA},
  year      = {1993},
  pages     = {13--28},
}

@inproceedings{pop-recPrin,
  author    = {Andrei Popescu and
               Elsa L. Gunter},
  title     = {Recursion principles for syntax with bindings and substitution},
  booktitle = {ICFP},
  year      = {2011},
  pages     = {346-358}
}

@INPROCEEDINGS{ms6,
  author={Zdancewic, S. and Myers, Andrew C.},
  booktitle={IEEE Computer Security Foundations Workshop},
  title={Observational determinism for concurrent program security},
  year={2003},
  pages={ 29--43},
  ISSN={1063-6900},
}

@inproceedings{DBLP:conf/plpv/AltenkirchMS07,
  author    = {Thorsten Altenkirch and
               Conor McBride and
               Wouter Swierstra},
  title     = {Observational equality, now!},
  booktitle = {PLPV},
  year      = {2007},
  pages     = {57-68}
}

@inproceedings{DBLP:conf/itp/Lammich13,
  author    = {Peter Lammich},
  title     = {Automatic Data Refinement},
  booktitle = {ITP},
  year      = {2013},
  pages     = {84-99}
}

@inproceedings{DBLP:conf/ccs/KovacsSF13,
  author    = {M{\'a}t{\'e} Kov{\'a}cs and
               Helmut Seidl and
               Bernd Finkbeiner},
  title     = {Relational abstract interpretation for the verification
               of 2-hypersafety properties},
  booktitle = {CCS},
  year      = {2013},
  pages     = {211-222}
}

@article{DBLP:journals/tse/FocardiG97,
  author    = {Riccardo Focardi and
               Roberto Gorrieri},
  title     = {The Compositional Security Checker: A Tool for the Verification
               of Information Flow Security Properties},
  journal   = {IEEE Trans. Software Eng.},
  volume    = {23},
  number    = {9},
  year      = {1997},
  pages     = {550-571}
}

@article{Manshaei:2013:GTM:2480741.2480742,
 author = {Manshaei, Mohammad Hossein and Zhu, Quanyan and Alpcan, Tansu and Bac\c{s}ar, Tamer and Hubaux, Jean-Pierre},
 title = {Game Theory Meets Network Security and Privacy},
 journal = {ACM Comput. Surv.},
 volume = {45},
 number = {3},
 year = {2013},
 pages = {25:1--25:39},
} 


@inproceedings{DBLP:conf/itp/LammichT12,
  author    = {Peter Lammich and
               Thomas Tuerk},
  title     = {Applying Data Refinement for Monadic Programs to Hopcroft's
               Algorithm},
  booktitle = {ITP},
  year      = {2012},
  pages     = {166-182}
}


@incollection{DBLP:reference/crypt/Mantel11,
  author    = {Heiko Mantel},
  title     = {Information Flow and Noninterference},
  booktitle = {Encyclopedia of Cryptography and Security (2nd Ed.)},
  year      = {2011},
  pages     = {605-607}
}

@unpublished{joana,
  title = "The {J}oana Website",
  note = "\url{http://pp.ipd.kit.edu/projects/joana}"
}


@inproceedings{jscript-flow,
 author = {Just, Seth and Cleary, Alan and Shirley, Brandon and Hammer, Christian},
 title = {Information Flow Analysis for {J}avascript},
 booktitle = {PLASTIC '11}, 
 year = {2011},
 pages = {9--18}
}

@misc{jif,
title = "Jif: {J}ava $+$ information flow",
note = "\url{http://www.cs.cornell.edu/jif}",
year = "2014"}

@inproceedings{DBLP:conf/cpp/MurrayMBGK12,
  author    = {Toby C. Murray and
               Daniel Matichuk and
               Matthew Brassil and
               Peter Gammie and
               Gerwin Klein},
  title     = {Noninterference for Operating System Kernels},
  booktitle = {CPP},
  year      = {2012},
  pages     = {126-142}
}

@book{gollman-2005,
 author = {Dieter Gollmann},
 title = {Computer Security},
 edition = "2nd",
 year = {2005},
 publisher = {Wiley}
}

@inproceedings{andy-nonfree,
  author    = {Andreas Schropp and
               Andrei Popescu},
  title     = {Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted
               Metatheory},
  booktitle = {CPP},
  year      = {2013},
  pages     = {114-130}
}

@inproceedings{DBLP:conf/post/ArapinisBR12,
  author    = {Myrto Arapinis and
               Sergiu Bursuc and
               Mark Ryan},
  title     = {Privacy Supporting Cloud Computing: ConfiChair, a Case Study},
  booktitle = {POST},
  year      = {2012},
  pages     = {89-108}
}


@inproceedings{Hic-MechanizedMetaReason,
  author    = {Jason Hickey and
               Aleksey Nogin and
               Xin Yu and
               Alexei Kopylov},
  title     = {Mechanized meta-reasoning using a hybrid {HOAS}/de {B}ruijn
               representation and reflection},
  booktitle = {ICFP},
  year      = {2006},
  pages     = {172--183},
}



@inproceedings{chlipala-Parametric,
  author    = {Adam J. Chlipala},
  title     = {Parametric higher-order abstract syntax for mechanized semantics},
  booktitle = {ICFP},
  year      = {2008},
  pages     = {143--156},
}


@article{harper-licata-LF,
  author    = {Robert Harper and
               Daniel R. Licata},
  title     = {Mechanizing metatheory in a logical framework},
  journal   = {J.~Funct. Program.},
  volume    = {17},
  number    = {4-5},
  year      = {2007},
  pages     = {613--673}
}




@inproceedings{licataUniverseOfBinding,
  author    = {Daniel R. Licata and
               Robert Harper},
  title     = {A universe of binding and computation},
  booktitle = {ICFP},
  year      = {2009},
  pages     = {123--134},
}

@inproceedings{stark-piSem,
  author    = {Ian Stark},
  title     = {A Fully Abstract Domain Model for the pi-Calculus},
  booktitle = {LICS 1996},
  year      = {1996},
  pages     = {36--42}
}

@article{deSimone,
 author = {R. de Simone},
 title = {Higher-level synchronizing devices in MEIJE-SCCS},
 journal = {Theor. Comput. Sci.},
 volume = {37},
 year = {1985},
 pages = {245--267},
 }

 @article{aceto-BisimulationBasedMethod,
  author    = {Luca Aceto and
               Matteo Cimini and
               Anna Ing{\'o}lfsd{\'o}ttir},
  title     = {A Bisimulation-based Method for Proving the Validity of
               Equations in GSOS Languages},
  journal   = {CoRR},
  volume    = {abs/1002.2864},
  year      = {2010},
}

@article{monProcEch,
  author    = {Raul Monroy and
               Alan Bundy and
               Ian Green},
  title     = {On Process Equivalence = Equation Solving in CCS},
  journal   = {J. Autom. Reasoning},
  volume    = {43},
  number    = {1},
  year      = {2009},
  pages     = {53--80},
}

@article{hen-ProofSysMesPas,
  author    = {Matthew Hennessy and H. Lin},
  title     = {Proof Systems for Message-Passing Process Algebras},
  journal   = {Formal Asp. Comput.},
  volume    = {8},
  number    = {4},
  year      = {1996},
  pages     = {379--407},
}

@inproceedings{DBLP:conf/cav/Strichman09,
  author    = {Ofer Strichman},
  title     = {Regression Verification: Proving the Equivalence of Similar
               Programs},
  booktitle = {CAV},
  year      = {2009},
  pages     = {63}
}

@article{mil-CompleteInferSys,
  author    = {Robin Milner},
  title     = {A Complete Inference System for a Class of Regular Behaviours},
  journal   = {J. Comput. Syst. Sci.},
  volume    = {28},
  number    = {3},
  year      = {1984},
  pages     = {439--466},
}

@inproceedings{gog-non,
  author    = {Joseph A. Goguen and Jos{\'e} Meseguer},
  title     = {Security Policies and Security Models},
  booktitle = {IEEE Symposium on Security and Privacy},
  year      = {1982},
  pages     = {11-20}
}



 @article{san-bis,
 author = {Sangiorgi,, Davide},
 title = {On the bisimulation proof method},
 journal = {Math. Struct. Comp. Sci.},
 volume = {8},
 number = {5},
 year = {1998},
 pages = {447--479},
}

  @inproceedings{fio-piSem,
  author    = {Marcelo P. Fiore and
               Eugenio Moggi and
               Davide Sangiorgi},
  title     = {A Fully-Abstract Model for the pi-Calculus (Extended Abstract)},
  booktitle = {LICS 1996},
  year      = {1996},
  pages     = {43--54},
}

 @inproceedings{gog-circCase,
  author    = {Joseph A. Goguen and
               Kai Lin and
               Grigore Ro\c{s}u},
  title     = {Conditional Circular Coinductive Rewriting with Case Analysis},
  booktitle = {WADT},
  year      = {2002},
  pages     = {216--232},
}

@inproceedings{DBLP:conf/cpp/BartheGKLB12,
  author    = {Gilles Barthe and
               Benjamin Gr{\'e}goire and
               C{\'e}sar Kunz and
               Yassine Lakhnech and
               Santiago Zanella B{\'e}guelin},
  title     = {Automation in Computer-Aided Cryptography: Proofs, Attacks
               and Designs},
  booktitle = {CPP},
  year      = {2012},
  pages     = {7-8}
}



@inproceedings{DBLP:conf/itp/EndrullisHB13,
  author    = {J{\"o}rg Endrullis and
               Dimitri Hendriks and
               Martin Bodin},
  title     = {Circular Coinduction in Coq Using Bisimulation-Up-To Techniques},
  booktitle = {ITP},
  year      = {2013},
  pages     = {354-369}
}



 @inproceedings{circCOCASL,
 author = {Daniel Hausmann, Till Mossakowski and Lutz Schr\"{o}der},
 title = {Iterative Circular Coinduction for \textsc{CoCasl} in {Isabelle\slash HOL}},
 booktitle = {FASE 2005},
 year = {2005},
 pages = {341--356},
 series = "LNCS",
 }

@inproceedings{morallyCorrect,
  author    = {Nils Anders Danielsson and
               John Hughes and
               Patrik Jansson and
               Jeremy Gibbons},
  title     = {Fast and loose reasoning is morally correct},
  booktitle = {POPL 2006},
  year      = {2006},
  pages     = {206--217}
}


@inproceedings{bruni-BisOpenTerms,
  author    = {Roberto Bruni and
               David de Frutos-Escrig and
               Narciso Mart\'{\i}-Oliet and
               Ugo Montanari},
  title     = {Bisimilarity Congruences for Open Terms and Term Graphs
               via Tile Logic},
  booktitle = {CONCUR 2000},
  year      = {2000},
  pages     = {259--274},
}

@article{rensnik-BisOpenTerms,
  author    = {Arend Rensink},
  title     = {Bisimilarity of Open Terms},
  journal   = {Inf. Comput.},
  volume    = {156},
  number    = {1-2},
  year      = {2000},
  pages     = {345--385},
}

@article{RuttenProcAsTerms,
  author    = {Jan J. M. M. Rutten},
  title     = {Processes as Terms: Non-Well-Founded Models for Bisimulation},
  journal   = {Math. Struct. Comp. Sci.},
  volume    = {2},
  number    = {3},
  year      = {1992},
  pages     = {257--275},
}


@inproceedings{circCALCO09theory,
  author    = {Grigore Ro\c{s}u and
               Dorel Lucanu},
  title     = {Circular Coinduction: A Proof Theoretical Foundation},
  booktitle = {CALCO'09},
  year      = {2009},
  pages     = {127--144}
}

@inproceedings{circCALCO07,
author = {Dorel Lucanu and Grigore Ro\c{s}u},
title= { {CIRC}: A Circular Coinductive Prover},
booktitle = {CALCO'07},
series = {LNCS},
year = {2007},
volume = {4624},
pages = {372--378}
}


@book{kriv-lambda,
  title = {Lambda-calculus, types and models},
  author = {J. L. Krivine},
  publisher = "Ellis Horwood",
  year = 1993,
  }

@book{MilCCSBook,
  title = {Communication and concurrency},
  author = {Robin Milner},
  publisher = "Prentice Hall",
  year = 1989,
  }

@article{mousavi-SOS,
  author    = {Mohammad Reza Mousavi and
               Michel A. Reniers and
               Jan Friso Groote},
  title     = {SOS formats and meta-theory: 20 years after},
  journal   = {Theor. Comput. Sci.},
  volume    = {373},
  number    = {3},
  year      = {2007},
  pages     = {238--272},
  ee        = {https://doi.org/10.1016/j.tcs.2006.12.019},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{bloom-GSOS,
 author = {Bloom,, Bard and Istrail,, Sorin and Meyer,, Albert R.},
 title = {Bisimulation can't be traced},
 journal = {J. ACM},
 volume = {42},
 number = {1},
 year = {1995},
 pages = {232--268},
 }

@book{MilPiBook,
  title = {Communicating and mobile systems: the $\pi$-calculus},
  author = {Robin Milner},
  publisher = "Cambridge",
  year = 2001,
}

@book{processAlgebra,
title = {Process {A}lgebra},
author = {J. C. M. Baeten and W. P. Weijland},
publisher = "Cambridge University Press",
year = 1990,
}


@inproceedings{howe-HOASInClassicalLogic,
  author    = {Douglass J. Howe},
  title     = {Higher-Order abstract syntax in classical higher-order logic},
  booktitle = {LFMTP},
  pages = "1--11",
  year      = {2009},
}




@incollection{gal-SNOverview,
author = "Jean Gallier",
title = "On {G}irard's Candidats de Reductibilite. ",
year = 1990,
booktitle = "Logic and Computer Science",
pages = "123--203",
publisher= "Academic Press",
}


@article{McAl-SNSystemFandBeyond,
  author = {McAllester and D. J. Kucan and D. F. Otth},
  title = {A Proof of Strong Normalization for {F}$_2$, {F}$_\omega$ and Beyond},
  journal   = {Inf. Comput.},
  volume    = {121},
  number    = {2},
  year      = {1995},
  pages     = {193--200},
}


@article{Ber-GenericityPi,
  author = {M. Berger and K. Honda and N. Yoshida},
  title = {Genericity and the Pi-Calculus},
  journal   = {Acta Inform.},
  volume    = {42},
  number    = {2},
  year      = {2005},
  pages     = {83--141},
}





@inproceedings{TC-original,

 author = {Honsell, Furio and Miculan, Marino and Scagnetto, Ivan},
 title = {An Axiomatic Approach to Metareasoning on Nominal Algebras in {HOAS}},
 booktitle = {ICALP},
 year = {2001},
 pages = {963--978},
 }




@inproceedings{Gab-NomRenSets,
  author    = {Murdoch James Gabbay and
               Martin Hofmann},
  title     = {Nominal Renaming Sets},
  booktitle = {LPAR},
  year      = {2008},
  pages     = {158--173},
}

@proceedings{lpar2008,
  editor    = {Iliano Cervesato and
               Helmut Veith and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning,
               15th International Conference, LPAR 2008, Doha, Qatar, November
               22-27, 2008. Proceedings},
  booktitle = {LPAR},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5330},
  year      = {2008},
}

@article{Buc-ConsitencyContexts,
  author    = {Anna Bucalo and
               Furio Honsell and
               Marino Miculan and
               Ivan Scagnetto and
               Martin Hofmann},
  title     = {Consistency of the theory of contexts},
  journal   = {J.~Funct. Program.},
  volume    = {16},
  number    = {3},
  year      = {2006},
  pages     = {327--372},
}

@article{mel-PiHOL,
  author    = {Thomas F. Melham},
  title     = {A Mechanized Theory of the Pi-Calculus in {HOL}},
  journal   = {Nord. J. Comput.},
  volume    = {1},
  number    = {1},
  year      = {1994},
  pages     = {50--76},
}

@inproceedings{DBLP:conf/middleware/HosekMPEESBP11,
  author    = {Petr Hosek and
               Matteo Migliavacca and
               Ioannis Papagiannis and
               David M. Eyers and
               David Evans and
               Brian Shand and
               Jean Bacon and
               Peter Pietzuch},
  title     = {SafeWeb: A Middleware for Securing Ruby-Based Web Applications},
  booktitle = {Middleware},
  year      = {2011},
  pages     = {491-511}
}

@inproceedings{jsflow,
  author    = {Daniel Hedin and Arnar Birgisson and Luciano Bello and Andrei Sabelfeld},
  title     = {{JSF}low: Tracking Information Flow in {J}avaScript and its APIs},
  booktitle = {SAC},
  year      = {2014}
}

@inproceedings{gimCoindCoq,
  author    = {Eduardo Gim{\'e}nez},
  title     = {An Application of Co-inductive Types in {C}oq: Verification
               of the Alternating Bit Protocol},
  booktitle = {TYPES'95},
  year      = {1995},
  pages     = {135--152},
}

@unpublished{CONCURtoolOverview,
title = "Verification Tools from the {CONCUR} project",
author = "Eric Madelaine",
note = "http://www-sop.inria.fr/meije/papers/concur-tools"}

@unpublished{hammer-jscript2,
title = "Information Flow Control in Webkit's {J}avaScript Bytecode",
author = "A Bichhawat and V Rajani and D Garg and C Hammer",
note = "To be presented at POST 2014"}


@unpublished{ECRINS,
title = "Proving process calculi translations in {ECRINS}: The pure{LOTOS} $\ra$ {MEIJE} example",
author = "Guillaume Doumenc and Eric Madelaine and Robert de Simone",
note = "Technical Report RR1192, INRIA, 1990. http://hal.archives-ouvertes.fr/inria-00075367/en/"}

@unpublished{de-auth,
title = "Automath, a language for mathematics",
author = "N. de Bruijn",
note = "Technical Report, Eindhoven University of Technology, 1967"}

@unpublished{mil-lcf,
title = "Logic for Computable Functions: description of a machine implementation",
author = "Robin Milner",
note = "Technical Report, Stanford University, 1972"}




@article{toolOverview,
  author    = {Paola Inverardi and
               Corrado Priami},
  title     = {Automatic Verification of Distributed Systems: The Process
               Algebra Approach},
  journal   = {Formal Methods in System Design},
  volume    = {8},
  number    = {1},
  year      = {1996},
  pages     = {7--38},
}

@article{muck-AutomatingSoundness,
  author    = {Muck van Weerdenburg},
  title     = {Automating Soundness Proofs},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {229},
  number    = {4},
  year      = {2009},
  pages     = {107--118},
}

@article{ruttenStreamCalculus,
  author    = {Jan J. M. M. Rutten},
  title     = {Elements of Stream Calculus (An Extensive Exercise in Coinduction)},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {45},
  year      = {2001},
}

@inproceedings{DBLP:conf/concur/Rutten98,
  author    = {Jan J. M. M. Rutten},
  title     = {Automata and Coinduction (An Exercise in Coalgebra)},
  booktitle = {CONCUR '98},
  year      = {1998},
  pages     = {194--218}
}

@article{BartelsGeneralizedCoind,
  author    = {Falk Bartels},
  title     = {Generalised Coinduction},
  journal   = {Math. Struct. Comp. Sci.},
  volume    = {13},
  number    = {2},
  year      = {2003},
  pages     = {321--348},
}

@article{damCyclicMu,
  author    = {Mads Dam and
               Dilian Gurov},
  title     = {$\mu$-calculus with explicit points and approximations},
  journal   = {J. Log. Comput.},
  volume    = {12},
  number    = {2},
  year      = {2002},
  pages     = {255--269},
}

@inproceedings{brothCyyclicProofsFOL,
  author    = {James Brotherston},
  title     = {Cyclic Proofs for First-Order Logic with Inductive Definitions},
  booktitle = {TABLEAUX'05},
  year      = {2005},
  pages     = {78--92},
}

@inproceedings{Locales,
  author    = {Florian Kamm{\"u}ller and
               Markus Wenzel and
               Lawrence C. Paulson},
  title     = {Locales---A Sectioning Concept for {I}sabelle},
  booktitle = {TPHOLs'99},
  year      = {1999},
  pages     = {149--166},
}

@inproceedings{IsabelleFramework,
  author    = {Makarius Wenzel and
               Lawrence C. Paulson and
               Tobias Nipkow},
  title     = {The Isabelle Framework},
  booktitle = {TPHOLs},
  year      = {2008},
  pages     = {33--38},
}


@misc{HOL4,
title = "The {HOL4} {T}heorem Prover",
note = "\url{http://hol.sourceforge.net}",
year = "2010"}


@inproceedings{urban-LFInNominal,
  author    = {Christian Urban and
               James Cheney and
               Stefan Berghofer},
  title     = {Mechanizing the Metatheory of LF},
  booktitle = {LICS 2008},
  year      = {2008},
  pages     = {45--56},
}



@article{rock-PiInIsabelle,
  author    = {Christine R{\"o}ckl and
               Daniel Hirschkoff},
  title     = {A fully adequate shallow embedding of the [pi]-calculus
               in {I}sabelle/{HOL} with mechanized syntax analysis},
  journal   = {J.~Funct. Program.},
  volume    = {13},
  number    = {2},
  year      = {2003},
  pages     = {415--451},
}





@INPROCEEDINGS{gacek08lfmtp,
  author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
  title = {Reasoning in {A}bella about Structural Operational
                  Semantics Specifications},
  year = 2008,
  booktitle = {LFMTP},
  pages = {75--89},
}

@inproceedings{DBLP:conf/cade/BohmeN10,
  author    = {Sascha B{\"o}hme and
               Tobias Nipkow},
  title     = {Sledgehammer: Judgement Day},
  booktitle = {IJCAR},
  year      = {2010},
  pages     = {107-121}
}

@INPROCEEDINGS{gacek08ijcar,
  author = {Andrew Gacek},
  title = {The {A}bella Interactive Theorem Prover
                  (System Description)},
  year = 2008,
  monthXXX = {August},
  booktitle = {Proceedings of IJCAR '08},
  pages = {154--161},
  volume = {5195},
  editor = {A. Armando and P. Baumgartner and G. Dowek},
}

@INPROCEEDINGS{gacek08lics,
  author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
  title = {Combining generic judgments with recursive
                 definitions},
  booktitle = {LICS 2008},
  monthXXX = {June},
  year = {2008},
  pages = {33--44},
  editor = {F. Pfenning},
}

@ARTICLE{mcDow-reas,
  author = {Raymond McDowell and Dale Miller},
  title = {Reasoning with Higher-Order Abstract Syntax in a
                 Logical Framework},
  journal = {ACM Transactions on Computational Logic},
  year = {2002},
  volume = {3},
  number = {1},
  pages = {80--136},
}

@inproceedings{feltyPientka-comparison,
  author    = {Amy P. Felty and
               Brigitte Pientka},
  title     = {Reasoning with Higher-Order Abstract Syntax and Contexts:
               A Comparison},
  booktitle = {ITP},
  year      = {2010},
  pages     = {227--242},
}


@article{mil-uni,
author = {Dale Miller and Gopalan Nadathur and Frank Pfenning and Andre Scedrov},
title = {Uniform Proofs as a Foundation for Logic Programming.},
journal = {Ann. Pure Appl. Logic}, volume = {51},
number = {1-2}, year = {1991},
 pages = {125--157}}

@ARTICLE{MillTiu-proofThGenJudg,
  author = {Dale Miller and Alwen Tiu},
  title = {A proof theory for generic judgments},
  journal = {ACM Transactions on Computational Logic},
  edited = {Phokion Kolaitis},
  volume = {6},
  number = {4},
  pages = {749--783},
  year = {2005},
}

@inproceedings{hyp2,
  author    = {Michael R. Clarkson and
               Bernd Finkbeiner and
               Masoud Koleini and
               Kristopher K. Micinski and
               Markus N. Rabe and
               C{\'e}sar S{\'a}nchez},
  title     = {Temporal Logics for Hyperproperties},
  booktitle = {POST},
  year      = {2014},
  pages     = {265-284}
}

@article{hyp1,
  author    = {Bernd Finkbeiner and
               Markus N. Rabe and
               C{\'e}sar S{\'a}nchez},
  title     = {A Temporal Logic for Hyperproperties},
  journal   = {CoRR},
  volume    = {abs/1306.6657},
  year      = {2013}
}

@article{Tiu-logReasGenJudg,
 author = {Alwen Tiu},
 title = {A Logic for Reasoning about Generic Judgments},
 journal = {Electron. Notes Theor. Comput. Sci.},
 volume = {174},
 number = {5},
 year = {2007},
 pages = {3--18},
 }









@article{stat-log,
  author    = {Richard Statman},
  title     = {Logical Relations and the Typed lambda-Calculus},
  journal   = {Information and Control},
  volume    = {65},
  number    = {2/3},
  year      = {1985},
  pages     = {85--97}
}

@inproceedings{ambler-primrecWeakHOAS,
  author    = {S. J. Ambler and
               Roy L. Crole and
               Alberto Momigliano},
  title     = {A definitional approach to primitive recursion over {H}igher
               {O}rder {A}bstract {S}yntax},
  booktitle = {MERLIN},
  year      = {2003},
}

@TECHREPORT{mom-Comparison,
    author = {A. Momigliano and S. J. Ambler and R. L. Crole},
    title = {A Comparison of Formalizations of the Meta-Theory of a Language with Variable Bindings in Isabelle},
    institution = {Supplemental Proceedings of TPHOL'01},
    year = {2001}
}

@inproceedings{mit-logSecondOrder,
 author = {John C. Mitchell and Albert R. Meyer},
 title = {Second-Order Logical Relations (Extended Abstract)},
 booktitle = {CLP},
 year = {1985},
 pages = {225--236},
 }

@inproceedings{mom-Hybrid1,
 author = {Simon Ambler and Roy L. Crole and Alberto Momigliano},
 title = {Combining {H}igher {O}rder {A}bstract {S}yntax with Tactical Theorem Proving and (Co)Induction},
 booktitle = {TPHOLs},
 year = {2002},
 pages = {13--30},
 }

 @inproceedings{mom-Hybrid2,
  author    = {Alberto Momigliano and
               Simon Ambler},
  title     = {Multi-level Meta-reasoning with Higher-Order Abstract Syntax},
  booktitle = {FoSSaCS 2003},
  year      = {2003},
  pages     = {375--391},
}


@inproceedings{urban-Barendregt,
  author    = {Christian Urban and
               Stefan Berghofer and
               Michael Norrish},
  title     = {Barendregt's Variable Convention in Rule Inductions},
  booktitle = {CADE},
  year      = {2007},
  pages     = {35--50},
}


@inproceedings{UrbanTasson,
  author    = {Christian Urban and
               Christine Tasson},
  title     = {Nominal Techniques in {I}sabelle/{HOL}},
  booktitle = {CADE},
  year      = {2005},
  pages     = {38--53}
}



@inproceedings{UrbanBerghof-RecCombNominal,
  author    = {Christian Urban and
               Stefan Berghofer},
  title     = {A Recursion Combinator for Nominal Datatypes Implemented
               in {I}sabelle/{HOL}},
  booktitle = {IJCAR},
  year      = {2006},
  pages     = {498--512}
}



@inproceedings{urban-Barendregt0,
  author    = {Christian Urban and
               Michael Norrish},
  title     = {A formal treatment of the {B}arendregt variable convention
               in rule inductions},
  booktitle = {MERLIN},
  year      = {2005},
  pages     = {25--32},
}


@inproceedings{felty-HypJudHybrid,
  author    = {Amy P. Felty and
               Alberto Momigliano},
  title     = {Reasoning with hypothetical judgments and open terms in
               {H}ybrid},
  booktitle = {PPDP},
  year      = {2009},
  pages     = {83--92},
}




@article{momFelty-Hybrid3,
 author = {Alberto Momigliano and Alan J. Martin and Amy P. Felty},
 title = {Two-Level {H}ybrid: A System for Reasoning Using {H}igher-{O}rder {A}bstract {S}yntax},
 journal = {Electron. Notes Theor. Comput. Sci.},
 volume = {196},
 year = {2008},
 pages = {85--93},
 }

@article{momFelty-Hybrid4,
  author    = {Amy P. Felty and
               Alberto Momigliano},
  title     = {Hybrid: A Definitional Two-Level Approach to Reasoning with
               {H}igher-{O}rder {A}bstract {S}yntax},
  journal   = {CoRR},
  volume    = {abs/0811.4367},
  year      = {2008},
}

@inproceedings{weakHOAS,
 author = {Jo\"{e}lle Despeyroux and Amy P. Felty and Andr\'{e} Hirschowitz},
 title = {Higher-Order Abstract Syntax in {C}oq},
 booktitle = {TLCA},
 year = {1995},
 pages = {124--138}
 }

 @inproceedings{strongHOASinCoq,
 author = {Jo\"{e}lle Despeyroux and Andr\'{e} Hirschowitz},
 title = {{H}igher-{O}rder {A}bstract {S}yntax with Induction in {C}oq},
 booktitle = {LPAR},
 year = {1994},
 pages = {159--173}
 }

 @article{urban-NominalHOL,
 author = {Urban,, Christian},
 title = {Nominal Techniques in {I}sabelle/{HOL}},
 journal = {J. Autom. Reason.},
 volume = {40},
 number = {4},
 year = {2008},
 pages = {327--356},
 }


 @inproceedings{gor-5axAlpha,
 author = {Gordon, Andrew D. and Melham, Thomas F.},
 title = {Five Axioms of Alpha-Conversion},
 booktitle = {TPHOLs '96: Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics},
 year = {1996},
 pages = {173--190},
 }

 @article{bru-lam,
title = "$\Lambda$-calculus notation with nameless dummies, a tool for automatic formula manipulation,
with application to the {C}hurch-{R}osser Theorem",
author = "N. de Bruijn",
journal = "Indag. Math",
volume = 34,
number = 5,
pages = "381--392",
year = 1972}


@article{norrish-MechanisingLambdaInFirstOrder,
  author    = {Michael Norrish},
  title     = {Mechanising lambda-calculus using a classical first order
               theory of terms with permutations},
  journal   = {Higher-Order and Symbolic Computation},
  volume    = {19},
  number    = {2-3},
  year      = {2006},
  pages     = {169--195},
}



@inproceedings{gor-deBruijn,
 author = {Gordon,, Andrew D.},
 title = {A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion},
 booktitle = {HUG '93: Proceedings of the 6th International Workshop on Higher
               Order Logic Theorem Proving and its Applications},
 year = {1994},
 isbn = {3-540-57826-9},
 pages = {413--425},
 }

 @inproceedings{primrecFOAS-Norrish04,
  author    = {Michael Norrish},
  title     = {Recursive Function Definition for Types with Binders},
  booktitle = {TPHOLs},
  year      = {2004},
  pages     = {241--256},
}

@inproceedings{deBruijnWorks-Norrish07,
  author    = {Michael Norrish and
               Ren{\'e} Vestergaard},
  title     = {Proof Pearl: De {B}ruijn Terms Really Do Work},
  booktitle = {TPHOLs},
  year      = {2007},
  pages     = {207--222}
}



@inproceedings{bas-meta,
 author = {David A. Basin and Robert L. Constable},
 title = {Metalogical frameworks},
 booktitle = {Logical environments},
 year = {1993},
 pages = {1--29},
 location = {Edinburgh, Scotland},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@inproceedings{Prospector,
  author    = {David Mandelin and
               Lin Xu and
               Rastislav Bod\'{\i}k and
               Doug Kimelman},
  title     = {Jungloid mining: helping to navigate the API jungle},
  booktitle = {PLDI},
  year      = {2005},
  pages     = {48--61}
}



@article{bar-gen,
  author    = {Henk Barendregt},
  title     = {Introduction to Generalized Type Systems},
  journal   = {J.~Funct. Program.},
  volume    = {1},
  number    = {2},
  year      = {1991},
  pages     = {125--154}
}


@inProceedings{har-fra,
    author = "Robert Harper and Furio Honsell and Gordon Plotkin",
    title = "A Framework for Defining Logics",
    booktitle = "LICS",
    pages = "194--204",
    year = "1987" }

@inproceedings{phe-hig,
 author = {F. Pfenning and C. Elliot},
 title = {Higher-order abstract syntax},
 booktitle = {PLDI},
 year = {1988},
 pages = {199--208}
 }

 @inproceedings{pitts01nominal,
author = {Andrew M. Pitts},
title = {Nominal Logic: A First Order Theory of Names and Binding.},
booktitle = {TACS},
year = {2001},
pages = {219--242}
 }

@inproceedings{hof-sem,
 author = {Martin Hofmann},
 title = {Semantical Analysis of Higher-Order Abstract Syntax},
 booktitle = {LICS 1999},
 year = {1999},
 pages = {204}
 }

 @article{phe-primRecHOAS,
 author = {Carsten Schurmann and Joelle Despeyroux and Frank Pfenning},
 title = {Primitive recursion for higher-order abstract syntax},
 journal = {Theor. Comput. Sci.},
 volume = {266},
 number = {1-2},
 year = {2001},
 pages = {1--57}
 }

 @inproceedings{pientka-POPLmark,
  author    = {Brigitte Pientka},
  title     = {Proof Pearl: The Power of Higher-Order Encodings in the
               Logical Framework LF},
  booktitle = {TPHOLs},
  year      = {2007},
  pages     = {246--261}
}



 @inproceedings{beluga,
  author    = {Brigitte Pientka},
  title     = {Beluga: Programming with Dependent Types, Contextual Data,
               and Contexts},
  booktitle = {FLOPS},
  year      = {2010},
  pages     = {1--12},
}



 @article{desp-primRecHOAS,
  author    = {Jo{\"e}lle Despeyroux and
               Pierre Leleu},
  title     = {Recursion over objects of functional type},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {11},
  number    = {4},
  year      = {2001},
  pages     = {555--572},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


 @inproceedings{PosSchur-PracProg,
  author    = {Adam Poswolsky and
               Carsten Sch{\"u}rmann},
  title     = {Practical Programming with Higher-Order Encodings and Dependent
               Types},
  booktitle = {ESOP},
  year      = {2008},
  pages     = {93--107},
  ee        = {https://doi.org/10.1007/978-3-540-78739-6_7},
  crossref  = {DBLP:conf/esop/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


 @phdthesis{mcdow-thesis,
title = "Reasoning in a logic with definitions and induction",
author = "Raymond Charles McDowell",
year = 1997,
school = "University of Pennsylvania"}

@article{ber-mod,
title = "Module Algebra",
author = "Jan Bergstra and Jan Heering and Paul Klint",
journal = "Journal of the Association for Computing Machinery",
volume = 37, number = 2,
pages = "335--372",
year = 1990}

@article{bergstra-heering-klint90-fsh,
title = "Module Algebra",
author = "J. Bergstra and J. Heering and P. Klint",
journal = "JACM",
volume = 37,
number = 2,
pages = "335--372",
year = 1990}


@inproceedings{bidoit-hennicker94-fsh,
author = "M. Bidoit and R. Hennicker",
title = "Proving Behavioural Theorems with Standard First-Order Logic",
booktitle = "Algebraic and Logic Programming (ALP'94)",
series = "LNCS",
volume = "850",
pages = "41--58",
year = "1994"}

@article{hen-com, author = {L. Henkin},
title = {Completeness in the theory of types},
 journal = {J. Symb. Log.},
 volume = {15}, number = {2}, year = {1950}, pages = {81--91}
}

@article{sun-alg, author = {Yong Sun},
title = {An Algebraic Generalization of {F}rege Structures---Binding Algebras},
 journal = {Theor. Comput. Sci.},
 volume = {211}, number = {1-2}, year = {1999}, pages = {189--232}
}

@article{hin-lam, author = {J. R. Hindley and G. Longo},
title = {Lambda calculus models and extensionality},
 journal = {Z. Math. Logik Grundlag Math.},
 volume = {29},  year = {1980}, pages = {289--310}
}

@inproceedings{ken-rel,
author = {Andrew Kennedy},
title = {Relational Parametricity and Units of Measure},
booktitle = {POPL 1997},
year = {1997},
pages = {442--455}
}

@incollection{aczel-final,
  author    = {Peter Aczel and
               Nax Paul Mendler},
  title     = {A Final Coalgebra Theorem},
  booktitle = {CTCS '89},
  year      = {1989},
  pages     = {357--365},
  editor    = {David H. Pitt and
               David E. Rydeheard and
               Peter Dybjer and
               Andrew M. Pitts and
               Axel Poign{\'e}},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {389},
}

%    author = {Aczel, Peter and Mendler, Nax},
%    booktitle = {Category Theory and Computer Science},
%    chapter = {21},
%    pages = {357--365},
%    series = {LNCS},
%    title = {{A final coalgebra theorem}},
%    publisher = "Springer",
%    year = {1989}

@inproceedings{mit-typeInfApp,
  author    = {John C. Mitchell},
  title     = {A Type-Inference Approach to Reduction Properties and Semantics
               of Polymorphic Expressions (Summary)},
  booktitle = {LISP and Functional Programming},
  year      = {1986},
  pages     = {308--319},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{acz-fre,
author = "P. Aczel",
title = "Frege Structures and Notations in Propositions, Truth and Set",
booktitle = "The Kleene Symposium",
publisher = "North Holland",
pages = "31--59",
year = "1980"}


@inproceedings{FiorePiLateStrBisSem,
  author    = {Marcelo P. Fiore and
               Eugenio Moggi and
               Davide Sangiorgi},
  title     = {A Fully-Abstract Model for the $\pi$-Calculus},
  booktitle = {LICS 1996},
  year      = {1996},
  pages     = {43--54},
}

@InProceedings{fio-abs,
author = {Marcelo Fiore and Gordon Plotkin and Daniele Turi},
title = {Abstract Syntax and Variable Binding (Extended Abstract)},
Booktitle={LICS 1999},
pages = {193--202},
year = {1999} }


@article{bru-sem,
author = "K. B. Bruce and A. R. Meyer and J. C. Mitchell",
title = "The semantics of second-order lambda calculus",
journal = "Information and Computation",
volume = 85,
number = 1,
pages = "76--134",
year = 1990}


@article{bidoit-hennicker96,
author = "Michel Bidoit and Rolf Hennicker",
title = "Behavioral Theories and the Proof of Behavioral Properties",
journal = "Theor.\ Comput.\ Sci.",
volume = 165,
number = 1,
pages = "3--55",
year = 1996}

@book{Constable-nuprl,
 author = {Constable, R. L. and Allen, S. F. and Bromley, H. M. and Cleaveland, W. R. and Cremer, J. F. and Harper, R. W. and Howe, D. J. and Knoblock, T. B. and Mendler, N. P. and Panangaden, P. and Sasaki, J. T. and Smith, S. F.},
 title = {Implementing mathematics with the Nuprl proof development system},
 year = {1986},
 publisher = {Prentice-Hall, Inc.}
} 

@article{bidoit-hennicker96-fsh,
author = "M. Bidoit and R. Hennicker",
title = "Behavioral Theories and the Proof of Behavioral Properties",
journal = "Theor.\ Comput.\ Sci.",
volume = 165,
number = 1,
pages = "3--55",
year = 1996}

@article{hennicker-wirsing-bidoit97,
title = "Proof systems for structured specifications with observability
  operators",
author = "Rolf Hennicker and Martin Wirsing and Michel Bidoit",
pages = "393--443",
journal = "Theor.\ Comput.\ Sci.",
monthXXX = feb,
year = "1997",
volume = "173",
number = "2"}


@book{aczel-NWF,
title = {Non-well-founded sets},
author = {Aczel, Peter},
publisher = "CSLI Lecture Notes, Stanford University",
year = 1988,
}

@book{coq,
title = {Interactive Theorem Proving and Program Development.
         Coq'Art: The Calculus of Inductive Constructions},
author = {Yves Bertot and Pierre Casteran},
publisher = "Springer",
year = 2004,
}

@book{nipkow-et-al-2002,
  author = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
  title = "{I}sabelle/{HOL}: A~Proof Assistant for Higher-Order Logic",
  publisher="Springer",
  year=2002}

@book{bar-lam,
title = {The Lambda Calculus},
author = {H. P. Barendregt},
publisher = "North-Holland",
year = 1984,
}

@book{mit-fou,
title = {Foundations for Programming Languages},
author = {J. C. Mitchell},
publisher = "MIT Press",
year = 1996,
}

@book{tro-basicProofTheory,
title = {Basic Proof Theory},
author = {A. S. Troelstra and H. Schwichtenberg},
publisher = "Cambridge University Press",
edition = "Second",
year = 2000,
}

@article{DBLP:journals/jfp/BernardyJP12,
  author    = {Jean-Philippe Bernardy and
               Patrik Jansson and
               Ross Paterson},
  title     = {Proofs for free - Parametricity for dependent types},
  journal   = {J. Funct. Program.},
  volume    = {22},
  number    = {2},
  year      = {2012},
  pages     = {107-152}
}

@book{bklos91-sh,
editor = "M. Bidoit and H.-J. Kreowski and
  P. Lescanne and F. Orejas and D. Sannella",
title = {Algebraic System Specification and Development. A Survey
  and Annotated Bibliography},
publisher = "Springer",
year = 1991,
volume = 501,
series = "LNCS"}

@article{birkhoff35,
title = "On the Structure of Abstract Algebras",
author = "Garrett Birkhoff",
year = 1935,
journal = "Proceedings of the Cambridge Philosophical Society",
volume = 31, pages = "433--454"}

@article{hue-HOAS,
  author    = {G{\'e}rard P. Huet and
               Bernard Lang},
  title     = {Proving and Applying Program Transformations Expressed with
               Second-Order Patterns},
  journal   = {Acta Inf.},
  volume    = {11},
  year      = {1978},
  pages     = {31--55}
}

@incollection{pfe-marktober,
author = "Frank Pfenning",
title = "Logical frameworks---A brief introduction.",
year = 2002,
booktitle = "Paris Colloqvium on Programming",
pages = "137--166",
publisher= "Kluwer Academic Publishers",
series ="NATO Science Series II",
volume = 62}

@inproceedings{conf/ifip/Reynolds83,
  author = {Reynolds, John C.},
  booktitle = {IFIP Congress},
  pages = {513-523},
  title = {Types, Abstraction and Parametric Polymorphism.},
  year = 1983
}


@incollection{rey-F,
author = "J. C. Reynolds",
title = "Towards a theory of type structure",
year = 1974,
booktitle = "Paris Colloqvium on Programming",
pages = "408--425",
publisher= "Springer",
series ="LNCS",
volume = 19}

@book{gir-proofsAsTypes,
author = "J.-Y. Girard",
title = "Proofs and Types",
publisher = "Cambridge University Press",
year = "1989"
}

@incollection{Tait1975,
  author="Tait, W. W.",
  title="A Realizability Interpretation of the
			Theory of Species",
  year=1975,
  booktitle="Logic Colloquium",
  publisher={Springer},
  pages="240--251",
}


@article{birkhoff-lipson70,
title = "Heterogenous Algebras",
author = "Garrett Birkhoff and J. D. Lipson",
year = 1970,
journal = "Journal of Combinatorial Theory",
volume = 8,
pages = "115--133"}

@book{birkhoff67,
key = "Birkhoff",
author = "Garrett Birkhoff",
title = "Lattice Theory",
publisher = "American Mathematical Society",
year = "1967",
volume = "25",
series = "American Mathematical Societ Colloquium Publications",
address = "New York, N.Y.",
edition = "Third edition",
annote = "Many references."}

@book{gun-sem,
author = "Carl A. Gunter",
title = "Semantics of Programming Languages. Structures and Techniques",
publisher = "MIT Press",
year = "1992"
}


@book{pie-typ,
author = "Benjamin C. Pierce",
title = "Types and Programming Languages",
publisher = "MIT Press",
year = "2002"
}

@incollection{blok-pigozzi92,
title = "Algebraic Semantics for Universal {H}orn Logic without Equality",
author = "Willem J. Blok and Don Pigozzi",
booktitle = "Universal Algebra and Quasigroup Theory",
editor = "A. Romanovska and J. Smith",
publisher = "Heldermann, Berlin",
year = 1992}

@article{bjm00,
author = "Adel Bouhoula and Jean-Pierre Jouannaud and Jos{\' e} Meseguer",
title = "Specification and proof in membership equational logic",
journal = "Theor.\ Comput.\ Sci.",
volume = 236,
pages = "35--132",
year = 2000}

@article{pau-genTh,
 author = {L. C. Paulson},
 title = {The foundation of a generic theorem prover},
 journal = {J. Autom. Reason.},
 volume = {5},
 number = {3},
 year = {1989},
}

@INPROCEEDINGS{mantel-genericSec,
    author = {Heiko Mantel and Andrei Sabelfeld},
    title = {A Generic Approach to the Security of Multi-Threaded Programs},
    booktitle = {CSFW},
    year = {2001},
    pages = {200--214}
}

@article{abramsky-FullAbstractionLazy,
 author = {Abramsky, Samson and Ong, C.-H. Luke},
 title = {Full abstraction in the lazy lambda calculus},
 journal = {Inf. Comput.},
 volume = {105},
 number = {2},
 year = {1993},
 issn = {0890-5401},
 pages = {159--267},
 doi = {https://doi.org/10.1006/inco.1993.1044},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
 }


@article{momigliano-HowesMethod,
  author    = {Alberto Momigliano and
               Simon Ambler and
               Roy L. Crole},
  title     = {A Hybrid Encoding of Howe's Method for Establishing Congruence
               of Bisimilarity},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {70},
  number    = {2},
  year      = {2002},
}

@article{howe-ProvingCongruenceOfBisimulation,
  author    = {Douglas J. Howe},
  title     = {Proving Congruence of Bisimulation in Functional Programming
               Languages},
  journal   = {Inf. Comput.},
  volume    = {124},
  number    = {2},
  year      = {1996},
}




@article{avr-usi,
 author = {Arnon Avron and Furio Honsell and Ian A. Mason and Robert Pollack},
 title = {Using typed $\lambda$-calculus to implement formal systems on a machine},
 journal = {J. of Aut. Reasoning},
 volume = {9},
 number = {3},
 year = {1992},
 pages = {309--354}
 }

@article{bjm00-fsh,
author = "A. Bouhoula and J.-P. Jouannaud and J. Meseguer",
title = "Specification and proof in membership equational logic",
journal = "Theor.\ Comput.\ Sci.",
volume = 236,
pages = "35--132",
year = 2000}


@article{broy-et-al87,
author = "Manfred Broy and Martin Wirsing and P. Pepper",
title = "On the algebraic definition of programming languages",
journal = "ACM Transactions on Programming Languages and Systems",
year = 1987,
volume = 9,
number = 1,
pages = "54--99",
monthXXX = jan}

@article{broy-et-al87-fsh,
author = "M. Broy and M. Wirsing and P. Pepper",
title = "On the algebraic definition of programming languages",
journal = "ACM Trans. on Prog. Lang. and Systems",
year = 1987,
volume = 9,
number = 1,
pages = "54--99",
monthXXX = jan}

@article{broy-wirsing82,
author = "Manfred Broy and Martin Wirsing",
title = "Partial Abstract Types",
journal = "Acta Informatica",
year = "1982",
volume = 18,
pages = "47--64"}

@article{broy-wirsing82-sh,
author = "M. Broy and M. Wirsing",
title = "Partial Abstract Types",
journal = "Acta Informatica",
year = "1982",
volume = 18,
pages = "47--64"}




@book{burmeister86,
author = "Peter Burmeister",
title = "A Model Theoretic Oriented Appraoch to Partial Algebras",
year = 1986,
publisher = "Akademie-Verlag Berlin"}

@book{tro-bas,
author = "A. S. Troelstra and H. Schwichtenberg",
title = "Basic Proof Calculus",
year = 1996,
publisher = "Cambridge University Press"}

@incollection{burstall-diacon94,
title = "Hiding and Behaviour: an Institutional Approach",
author = "Rod Burstall and R\u{a}zvan Diaconescu",
booktitle = "A Classical Mind: Essays in Honour of C. A. R. Hoare",
editor = "A. William Roscoe",
publisher = "Prentice-Hall",
pages = "75--92",
year = 1994,
note = "Also in Technical Report ECS-LFCS-8892-253, Laboratory for
Foundations
  of Computer Science, University of Edinburgh, 1992"}

@incollection{burstall-diacon94-fsh,
title = "Hiding and Behaviour: an Institutional Approach",
author = "R. Burstall and R. Diaconescu",
booktitle = "A Classical Mind: Essays in Honour of C. A. R. Hoare",
publisher = "Prentice Hall",
pages = "75--92",
year = 1994}

@incollection{bd94,
title = "Hiding and Behaviour: an Institutional Approach",
author = "Rod Burstall and R\u{a}zvan Diaconescu",
booktitle = "A Classical Mind: Essays in Honour of C. A. R. Hoare",
editor = "A.~William Roscoe",
publisher = "Prentice-Hall",
pages = "75--92",
year = 1994,
note = "Also Technical Report ECS-LFCS-8892-253, Laboratory for Foundations
  of Computer Science, University of Edinburgh, 1992"}

@incollection{bd94-sh,
title = "Hiding and Behaviour: an Institutional Approach",
author = "Rod Burstall and R\u{a}zvan Diaconescu",
booktitle = "A Classical Mind: Essays in Honour of C. A. R. Hoare",
editor = "A.~William Roscoe",
publisher = "Prentice-Hall",
pages = "75--92",
year = 1994}


@inproceedings{nip-finiteSetsIterator,
  author    = {Tobias Nipkow and
               Lawrence C. Paulson},
  title     = {Proof Pearl: Defining Functions over Finite Sets},
  booktitle = {TPHOLs},
  year      = {2005},
  pages     = {385--396},
}


@inproceedings{Isar,
  author    = {Markus Wenzel},
  title     = {{I}sar---A Generic Interpretative Approach to Readable Formal
               Proof Documents},
  booktitle = {TPHOLs},
  year      = {1999},
  pages     = {167--184}
}


@inproceedings{Isar2,
author={Tobias Nipkow},
title={{Structured Proofs in {I}sar\slash {HOL}}},
booktitle={TYPES},
year=2003,
pages={259--278}
}

@article{cur-CategoricalCombinators,
  author    = {Pierre-Louis Curien},
  title     = {Categorical Combinators},
  journal   = {Information and Control},
  volume    = {69},
  number    = {1-3},
  year      = {1986},
  pages     = {188--254}
}

@article{oht-SubstLemmaDeBruijn,
  author    = {Hiroshi Ohtsuka},
  title     = {A Proof of the Substitution Lemma in de {B}ruijn's Notation},
  journal   = {Inf. Process. Lett.},
  volume    = {46},
  number    = {2},
  year      = {1993},
  pages     = {63--66}
}




@inproceedings{ATS,
  author    = {Chiyan Chen and
               Hongwei Xi},
  title     = {Combining programming with theorem proving},
  booktitle = {ICFP},
  year      = {2005},
  pages     = {66--77},
}


@article{don-SN,
 author = {Donnelly, Kevin and Xi, Hongwei},
 title = {A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System {F}},
 journal = {Electron. Notes Theor. Comput. Sci.},
 volume = {174},
 number = {5},
 year = {2007},
 pages = {109--125},
 }



@unpublished{LEGO,
title = "{LEGO}",
note = "http://www.dcs.ed.ac.uk/home/lego"}



@unpublished{delphin,
title = "Delphin",
note = "http://cs-www.cs.yale.edu/homes/carsten/delphin"}


@unpublished{Loa-NormalizationByCalculation,
title = "Normalization by calculation",
author = "R. Loader",
note = "Unpublished note, 1995. http://homepages.ihug.co.nz/~suckfish/papers/normal.pdf"}

@unpublished{urbanGeneralBinders,
title = "General {B}inders and {A}lpha-{E}quivalence in {N}ominal {I}sabelle",
author = "Christian Urban and Cezary Kaliszyk",
note = "To appear in ESOP 2011. Available online at \url{http://www4.intum.de/~urbanc/publications.html}"}

@unpublished{bg78,
title = "Semantics of {C}lear",
author = "Rod Burstall and Joseph Goguen",
year = 1978,
note = "Unpublished notes handed out at the 1978 Symposium on Algebra and
  Applications, Stefan Banach Center, Warsaw, Poland"}

@incollection{bg80,
author = "Rod Burstall and Joseph Goguen",
title = "The Semantics of {C}lear, a Specification Language",
booktitle = "Proceedings, 1979 Copenhagen Winter School on
  Abstract Software Specification",
editor = "Dines Bjorner",
note = "LNCS, Volume 86; based on unpublished
  notes handed out at the Symposium on Algebra and Applications, Stefan
  Banach Center, Warsaw, Poland, 1978",
publisher = "Springer",
pages = "292--332",
year = 1980}

@incollection{burstall-goguen80,
author = "Rod Burstall and Joseph Goguen",
title = "{The Semantics of {C}lear, a Specification Language}",
booktitle = "Proceedings, 1979 Copenhagen Winter School on
  Abstract Software Specification",
editor = "Dines Bjorner",
series = "LNCS",
volume = "86",
publisher = "Springer",
pages = "292--332",
year = 1980}

@article{DBLP:journals/tcs/MayrN98,
  author    = {Richard Mayr and
               Tobias Nipkow},
  title     = {Higher-Order Rewrite Systems and Their Confluence},
  journal   = {Theor. Comput. Sci.},
  volume    = {192},
  number    = {1},
  year      = {1998},
  pages     = {3--29}
}

@article{burstall-landin69,
author = "Rod Burstall and P. Landin",
title = "Programs and their proofs: an algebraic approach",
journal = "Machine Intelligence",
year = "1969",
volume = "4",
pages = "17--43",
note = {Edinburgh University Press, eds. B. Meltzer, D. Michie}}

@article{burstall-landin69-fsh,
author = "R. Burstall and P. Landin",
title = "Programs and their proofs: an algebraic approach",
journal = "Machine Intelligence",
year = "1969",
volume = "4",
pages = "17--43",
note = {Edinburgh University Press}}

@book{boehm81,
author = "B. Boehm",
title = "Software Engineering Economics",
publisher = "Prentice-Hall",
year = "1981"}

@inproceedings{buss-rosu00,
title = "Incompleteness of Behavioral Logics",
author = "Samuel Buss and Grigore Ro\c{s}u",
booktitle = {Proceedings of Coalgebraic Methods in Computer Science
  (CMCS'00), Berlin, Germany, March 2000},
publisher = "Elsevier Science",
editor = "Horst Reichel",
volume = 33,
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
pages = "61--79",
year = 2000}

@inproceedings{pfe-logicalFrameworksHandbookChapter,
title = "Logical frameworks",
author = "Frank Pfenning",
booktitle = {Handbook of Automated Reasoning},
publisher = "Elsevier Science",
year = 1999}


@inproceedings{gir-F,
title = "Une extension de l'interpretation de {G}{\"o}del a l'analyse, et
son application a l'elimination des coupure dans l'analyse et la theorie des types",
author = "J.-Y. Girard",
year = 1971,
booktitle = "2nd Scandinavian Logic Symposium",
pages = "63--92",
}

@inproceedings{Bar-LambdaCalculiWithTypes,
title = "Lambda Calculi with Types",
author = "Henkt Barendregt",
booktitle = {Handbook of Logic in Computer Science},
publisher = "Oxford University Press",
editor = "S. Abramsky and D. M. Gabbay and T. S. E. Maibaum",
year = "1992"}

@inproceedings{buss-rosu00-fsh,
title = "Incompleteness of Behavioral Logics",
author = "S. Buss and G. Ro\c{s}u",
booktitle = "Proceeding of CMCS'00",
publisher = "Elsevier",
volume = 33,
series = "ENTCS",
pages = "61--79",
year = 2000}

@unpublished{casl,
key = "cofi",
title = {{CoFI} Task Group on Semantics,
  {CASL} --- {T}he {C}ommon {A}lgebraic {S}pecification {L}anguage, {S}emantics},
monthXXX = jul,
year = 1999,
note = "www.brics.dk/Projects/CoFI/Documents/CASL"}


@article{cazanescu72,
title = "Familles initiales et finales",
author = "Virgil Emil C\u{a}z\u{a}nescu",
journal = "Revue Roumaine de Mathematiques et Appliques",
year = 1972,
volume = 17,
number = 6}

@incollection{cazanescu93,
title = "Local equational logic",
author = "Virgil C\u{a}z\u{a}nescu",
year = 1993,
booktitle = "Proceedings,  9th International Conference on Fundamentals of
  Computation Theory FCT'93",
editor = "Zoltan Esik",
publisher = "Springer",
pages = "162--170",
note = "LNCS, Volume 710"}

@incollection{cazanescu94,
title = "Local equational logic 2",
author = "Virgil C\u{a}z\u{a}nescu",
year = 1994,
booktitle = "Developments in Language Theory: At The Crossroads of
  Mathematics, Computer Science and Biology",
editor = "G. Rosenberg and A. Saloma",
publisher = "World Scientific",
pages = "210--221"}

@article{caza-rosu97,
title = "Weak Inclusion Systems",
author = "Virgil Emil C\u{a}z\u{a}nescu and Grigore Ro\c{s}u",
pages = "195--206",
journal = "Mathematical Structures in Computer Science",
year = 1997,
volume = 7,
number = 2}

@article{caza-stef91,
title = "Classes of finite relations as initial abstract data types 1",
author = "Virgil Emil C\u{a}z\u{a}nescu and Gheorghe \c Stefanescu",
journal = "Discrete Mathematics",
year = 1991,
volume = 90,
pages="233--265"}

@article{smyth-powerDomains,
  author    = {Michael B. Smyth},
  title     = {Power Domains},
  journal   = {J. Comput. Syst. Sci.},
  volume    = {16},
  number    = {1},
  year      = {1978},
  pages     = {23--36}
}

@inproceedings{krauss-fun,
  author    = {Alexander Krauss},
  title     = {Partial Recursive Functions in Higher-Order Logic},
  booktitle = {IJCAR},
  year      = {2006},
  pages     = {589--603}
}

@article{caza-stef94,
title = "Classes of finite relations as initial abstract data types 2",
author = "Virgil Emil C\u{a}z\u{a}nescu and Gheorghe \c Stefanescu",
journal = "Discrete Mathematics",
year = 1994,
volume = 126,
pages="47--65"}

@phdthesis{cerioli-thesis,
title = "Relationships between Logical Frameworks",
author = "Maura Cerioli",
year = 1993,
school = "Universities of Genova, Pisa and Udine"}

@phdthesis{ken-the,
title = "Programming Languages and Dimension",
author = "Andrew Kennedy",
year = 1996,
school = "University of Cambridge"}

@inproceedings{corbett-et-al00,
author = "James Corbett and Matthew B. Dwyer and John Hatcliff and
  Corina S. Pasareanu and Robby and Shawn Laubach and Hongjun Zheng",
title  = "{Bandera : Extracting Finite-state Models from Java Source Code}",
booktitle= "Proceedings of the 22nd International Conference on
  Software Engineering",
address = "Limerick, Ireland",
month  = jun,
publisher = "ACM",
year   = 2000}

@techreport{cerioli-gogolla94,
author ="Martin Gogolla and Maura Cerioli",
title ="What is an {A}bstract {D}ata {T}ype after all?",
institution ="DISI -- University of Genova",
year =1994}

@techreport{cerioli-gogolla94-sh,
author ="M. Gogolla and M. Cerioli",
title ="What is an {A}bstract {D}ata {T}ype after all?",
institution ="DISI -- University of Genova",
year =1994}

@article{cerioli-meseguer97,
title = "May {I} Borrow Your Logic? ({T}ransporting Logical Structures
  along Maps)",
author = "Maura Cerioli and Jos{\' e} Meseguer",
year = 1997,
journal = "Theor.\ Comput.\ Sci.",
volume = 173,
number = 2,
pages = "311--347"}

@article{cerioli-meseguer97-fsh,
title = "May {I} Borrow Your Logic? ({T}ransporting Logical Structures
  along Maps)",
author = "M. Cerioli and J. Meseguer",
year = 1997,
journal = "Theor.\ Comput.\ Sci.",
volume = 173,
number = 2,
pages = "311--347"}

@incollection{cerioli-mossakowski-reichel98,
author = "Maura Cerioli and Till Mossakowski and Horst Reichel",
title = "From Total Equational to Partial First Order",
booktitle = "Algebraic Foundation of Information Systems Specification",
editor = "E. Astesiano and H.-J. Kreowski and B. Krieg-Bruckner",
pages = "31--104",
year = "1999",
publisher = "Springer Verlag",
note = "Chapter 3.  A preliminary version is in DISI-TR-96, 1996"}

@book{cha-mod,
title = "Model Theory",
author = "C. C. Chang and H. J. Keisler",
year = 1973,
publisher = "North Holland, Amsterdam"}

@misc{cirstea96,
author = "Corina C\^{\i}rstea",
title = "A Semantical Study of the Object Paradigm",
note = "Thesis submitted for transfer to DPhil status, University of
  Oxford, 1996"}

@incollection{cirstea97-fsh,
author = "C. C{\^\i}rstea",
title = "Coalgebra Semantics for Hidden Algebra:
  parameterized objects and inheritance",
booktitle = "Recent Trends in Algebraic Development Techniques",
publisher = "Springer",
volume = "1376",
series = "LNCS",
year = "1998"}

@inproceedings{cirstea99,
title = "A Coequational Approach to Specifying Behaviours",
author = "Corina C{\^\i}rstea",
booktitle = {Proceedings of the Second Workshop on Coalgebraic Methods
  in Computer Science (CMCS'99), Amsterdam, The Netherlands, March 1999},
publisher = "Elsevier Science",
volume = 19,
editor = "Bart Jacobs and Jan Rutten",
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
year = 1999}

@inproceedings{cirstea99-fsh,
title = "A Coequational Approach to Specifying Behaviours",
author = "C. C{\^\i}rstea",
booktitle = {Proceedings of CMCS'99},
publisher = "Elsevier",

volume = 19,
series = "ENTCS",
year = 1999}

@misc{cmw99,
title = "Order Sorted Hidden Algebra",
author = "Corina C\^{\i}rstea and Grant Malcolm and James Worrell",
year = 1999,
note= "Computing Laboratory, Oxford University.  Draft."}

@incollection{cirstea99b,
editor = "Jos\'{e} Luiz Fiadeiro",
author = "Corina C{\^\i}rstea",
title = "Semantic Constructions for Hidden Algebra",
booktitle = "Recent Trends in Algebraic Development Techniques",
publisher = "Springer",
volume = "1589",
series = "LNCS",
year = "1999"}

@incollection{cirstea99b-fsh,
author = "C. C{\^\i}rstea",
title = "Semantic Constructions for Hidden Algebra",
booktitle = "Recent Trends in Algebraic Development Techniques",
publisher = "Springer",
volume = "1589",
series = "LNCS",
year = "1999"}

@article{clark85,
author = "David Clark",
title =  "The Structuring of Systems Using Upcalls",
pages =  "171--180",
journal ="SIGOPS (Special Interest Group on Operating Systems)",
volume = "19",
number = "5",
monthXXX =  dec,
year =   "1985"}

@article{clarke-et-al96,
author = "Edmund M. Clarke and Jeannette M. Wing and Rajeev Alur
  and Rance Cleaveland and David Dill and Allen Emerson
  and Stephen Garland and Steven German and John Guttag
  and Anthony Hall and Thomas Henzinger and Gerard
  Holzmann and Cliff Jones and Robert Kurshan and Nancy
  Leveson and Kenneth McMillan and J. Moore and Doron
  Peled and Amir Pnueli and John Rushby and Natarajan
  Shankar and Joseph Sifakis and Prasad Sistla and
  Bernhard Steffen and Pierre Wolper and Jim Woodcock and
  Pamela Zave",
title = "Formal methods: state of the art and future directions",
journal = "ACM Computing Surveys",
volume = "28",

number = "4",
pages = "626--643",
monthXXX = dec,
year = "1996"}

@inproceedings{clavel-et-al96,
author = "Manuel Clavel and Steven Eker and Patrick Lincoln and
  Jos\'e Meseguer",
title = "Principles of {M}aude",
editor = "Jos\'e Meseguer",
volume = "4",
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
pages = "65--89",

booktitle = "Proceedings of the First International Workshop on
  Rewriting Logic",
year = "1996",
organization = "Elsevier"}

@inproceedings{maude,
author = "Manuel Clavel and Francisco J. Dur{\'a}n and Steven Eker and
  Patrick Lincoln and Narciso Mart{\'\i}-Oliet and Jos\'e Meseguer and
  Jos\'e F. Quesada",
title = "The {Maude} System",
editor = "Paliath Narendran and Micha$\ddot{\rm e}$l Rusinowitch",
pages = "240--243",
booktitle = "Proceedings of the 10th International Conference on
  Rewriting Techniques and Applications (RTA-99)",
year = "1999",
series = "LNCS",
volume = "1631",
publisher = "Springer",
address = "Trento, Italy",
monthXXX = jul,
note = "System Description",
keywords = "rewriting"}

@misc{maudea,
author = "Manuel Clavel and Francisco J. Dur{\'a}n and Steven Eker and
  Patrick Lincoln and Narciso Mart{\'\i}-Oliet and Jos\'e Meseguer and
  Jos\'e F. Quesada",
title = "Maude: {Specification and Programming in Rewriting Logic}",
year = "1999",
monthXXX = mar,
note = "Maude System documentation at {\tt http://maude.csl.sri.com/papers}"}

@article{clavel-et-al02,
author = "Manuel Clavel and Francisco J. Dur{\'a}n and Steven Eker and
  Patrick Lincoln and Narciso Mart{\'\i}-Oliet and Jos\'e Meseguer and
  Jos\'e F. Quesada",
title = "Maude: {Specification and Programming in Rewriting Logic}",
year = "2002",
journal = "Theor.\ Comput.\ Sci.",
volume = "285",
pages = "187--243"}

@article{clavel-et-al02-fsh,
author = "M. Clavel and F. J. Dur{\'a}n and S. Eker and P. Lincoln and
  N. Mart{\'\i}-Oliet and J. Meseguer and J. F. Quesada",
title = "Maude: {Specification and Programming in Rewriting Logic}",
year = "2002",
journal = "Theor.\ Comput.\ Sci.",
volume = "285",
pages = "187--243"}

@misc{clavel-et-al00,
author = "Manuel Clavel and Francisco J. Dur{\'a}n and Steven Eker and
  Patrick Lincoln and Narciso Mart{\'\i}-Oliet and Jos\'e Meseguer and
  Jos\'e F. Quesada",
title = "{A Maude Tutorial}",
year = "2000",
monthXXX = mar,
note = "Manuscript at {\tt http://maude.csl.sri.com/papers}"}

@incollection{maude96,
title = "Principles of {M}aude",
author = "Manuel Clavel and Steven Eker and Patrick Lincoln and Jos\'{e}
  Meseguer",
year = 1996,
booktitle = "Proceedings, First International Workshop on Rewriting
  Logic and its Applications",
editor = "Jos\'{e} Meseguer",
publisher = "Elsevier Science",
note = "Volume 4, {\it Electr.\ Notes Theor.\ Comput.\ Sci.}"}

@incollection{maude96-fsh,
title = "Principles of {M}aude",
author = "M. Clavel and S. Eker and P. Lincoln and J. Meseguer",
year = 1996,
booktitle = "Proceedings of WRLA",
publisher = "Elsevier",
series = "ENTCS",
volume = 4}


@article{pol-LocNamed1,
author = "Masahiko Sato and Robert Pollack",
title = "External and Internal Syntax of the Lambda-calculus",
journal = "Journal of Symbolic Computation",
volume = "45",
pages = "598--616",
year = "2010"}


@unpublished{pol-LocNamed2,
author = {Robert Pollack and Masahiko Sato},
title = "A Canonical Locally Named Representation of Binding",
note = "To appear in Journal of Automated Reasoning."}


@inproceedings{pol-PureTypeSystmesFormalized,
  author    = {James McKinna and
               Robert Pollack},
  title     = {Pure Type Systems Formalized},
  booktitle = {TLCA},
  year      = {1993},
  pages     = {289--305},
}



@unpublished{maude-manual,
author = "Manuel Clavel and Francisco Dur\'an and Steven Eker and
  Patrick Lincoln and Narciso Mart\'{\i}-Oliet and Jos\'e Meseguer and
  Jos\'e Quesada",
title = "Maude: specification and programming in rewriting logic",
note = {SRI International, January 1999,
  {\footnotesize\tt http://maude.csl.sri.com}}}

@unpublished{maude-manual-fsh,
author = "M. Clavel and F. Dur\'an and S. Eker and
  P. Lincoln and N. Mart\'{\i}-Oliet and J. Meseguer and
  J. Quesada",
title = "Maude: specification and programming in rewriting logic",
note = {SRI International, January 1999, \url{http://maude.csl.sri.com}}}

@inproceedings{clavel01towards,
author = {Manuel Clavel and Francisco Dur\'an and Steven Eker and
  Patrick Lincoln and Narciso Marti-Oliet and Jos\'e Meseguer and
  Jos\'e Quesada},
title = "{Towards Maude 2.0}",
booktitle = "Proceedings of the 3rd International Workshop on Rewriting Logic
  and its Applications",
editor = "Kokichi Futatsugi",
year = 2000,
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
volume = 36,
publisher = "Elsevier"}

@inproceedings{DBLP:conf/afp/McBride04,
  author    = {Conor McBride},
  title     = {Epigram: Practical Programming with Dependent Types},
  booktitle = {Advanced Functional Programming},
  year      = {2004},
  pages     = {130-170}
}

@unpublished{itp-manual,
author = "Manuel Clavel",
title = "{ITP} Tool",
note = {Department of Philosophy, University of Navarre,
  {\footnotesize\tt http://sophia.unav.es/~clavel/itp/}}}

@inproceedings{clavel01towards-fsh,
author = {M. Clavel and F. Duran and S. Eker and P. Lincoln and
  N. Marti-Oliet and J. Meseguer and J. F. Quesada},
title = "{Towards Maude 2.0}",
booktitle = {Proceedings of WRLA'01},
series = "ENTCS",
volume = {36}}

@book{Beckert:2007:VOS:1808999,
 author = {Beckert, Bernhard and H\"{a}hnle, Reiner and Schmitt, Peter H.},
 title = {Verification of Object-oriented Software: The KeY Approach},
 year = {2007},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 

@inproceedings{cafe-tools-entcs,
author = "Manuel Clavel and Francisco Dur\'an and Steven Eker and
  Jos\'e Meseguer",
title = "Building equational proving tools by reflection in rewriting
logic",
year = 2000,
booktitle = {CAFE: An Industrial-Strength Algebraic Formal Method},
publisher = "Elsevier",
note = {\url{http://maude.csl.sri.com}}}

@inproceedings{cafe-tools-entcs-fsh,
author = "M. Clavel and F. Dur\'an and S. Eker and
  J. Meseguer",
title = "Building equational proving tools by reflection in rewriting
logic",
year = 2000,
booktitle = {CAFE: An Industrial-Strength Algebraic Formal Method},
publisher = "Elsevier",
note = {\url{http://maude.csl.sri.com}}}

@book{clavel00,
author = "Manuel Clavel",
title = "Reflection in Rewriting Logic: Metalogical Foundations and
  Metaprogramming Applications",
year = "2000",
publisher = "CSLI Publications"}

@article{clavel-meseguer00,
author = "Manuel Clavel and Jos\'e Meseguer",
title = "Reflection in conditional rewriting logic",
journal = "Theor.\ Comput.\ Sci.",
volume = "304",
number = "1-2",
year = "2003, to appear"}

@misc{cofi,
author = "CoFI",
title  = "{\sc casl} Summary",
note = "{\small{\tt www.brics.dk/Projects/CoFi}}",
year = 2000}

@incollection{corradini97,
author = "Andrea Corradini",
title = "A Complete Calculus for Equational Deduction in Coalgebraic
  Specification",
year = 1997,
booktitle = "Recent Trends in Algebraic Development Techniques",
publisher = "Springer",
volume = "1376",
series = "LNCS"}

@incollection{corradini97-fsh,
author = "A. Corradini",
title = "A Complete Calculus for Equational Deduction in Coalgebraic
  Specification",
year = 1997,
booktitle = "Proceedings WADT'97",
publisher = "Springer",
volume = "1376",
series = "LNCS"}

@inproceedings{corradini-etal-99-fsh,
title = "From {SOS} specifications to structured coalgebras:
  How to Make Bisimulation a Congruence",
author = "A. Corradini and R. Heckel and U. Montanari",
booktitle = "Proceedings of CMCS'99",
publisher = "Elsevier",
volume = 19,
series = "ENTCS",
year = 1999}

@article{corradini-heckel-montanari02,
author = "Andrea Corradini and R. Heckel and Ugo Montanari",
title = "Compositional {SOS} and Beyond: A Coalgebraic View of Open Systems",
journal = "Theor.\ Comput.\ Sci.",
year = "To appear"}

@article{cra-lin,
title = "Linear Reasoning.  {A} new form of the {H}erbrand-{G}entzen {T}heorem",
author = "W. Craig",
journal = "J. Symb. Log.",
volume = 22,
year = 1957,
pages = "250--268"}

@techreport{curzon92,
author = "Paul Curzon",
title = "Of What Use is a Verified Compiler Specification?",
institution = "University of Cambridge, Computer Laboratory",
year = "1992",

type = "Technical Report",
number = "274"}

@article{demartini-iosif-sisto99,
author = "Claudio Demartini and Radu Iosif and Riccardo Sisto",
title = "{A Deadlock Detection Tool for Concurrent Java Programs}",
journal = "Software Practice and Experience",
volume = "29",
number = "7",
pages = "577--603",
monthXXX = jul,
year = 1999}

@inproceedings{dennis96,
title = "Using a generalisation critic to find bisimulations for
  coinductive proofs",
author = "Louise Dennis and Alan Bundy and Ian Green",
publisher = "Springer",
series = "Lecture Notes in Artificial Inteligence",
editor = "William McCune",
volume = 1249,
pages = {276--290},
year = 1996,
booktitle = "Proceedings of the 14th Conference on Automated Deduction"}

@incollection{dia-log,
author = "R\u{a}zvan Diaconescu and Joseph Goguen and Petros Stefaneas",
title = "Logical Support for Modularization",
booktitle = "Logical Environments",
editor = "Gerard Huet and Gordon Plotkin",
publisher = "Cambridge",
pages = "83--130",
year = 1993}

@incollection{modalg-fsh,
author = "R. Diaconescu and J. Goguen and P. Stefaneas",
title = "Logical Support for Modularization",
booktitle = "Logical Environments",
publisher = "Cambridge",
pages = "83--130",
year = 1993}

@techreport{diacon90,
author = "R\u{a}zvan Diaconescu",
title = "The Logic of {H}orn Clauses is Equational",
institution = "Programming Research Group, University of Oxford",
number = "PRG--TR--3--93",
year = 1993,
note ="Written in 1990"}

@techreport{diacon96,
title = "Completeness of Semantic Paramodulation: a Category-based
  Approach",
author = "R\u{a}zvan Diaconescu",
year = 1996,
institution = "Japan Advanced Institute for Science and Technology",
number = "IS-RR-96-0006S"}

@misc{diacon96b,
title = "Behavioral Rewriting Logic: semantic foundations and proof theory",
author = "R\u{a}zvan Diaconescu",
year = 1996,
monthXXX = "October",
journal = "Journal of Computer and System Sciences",
note= "Submitted for publication."}

@inproceedings{diacon96d,
title = "A Category-based Equational Logic Semantics to Constraint
  Programming",
author = "R\u{a}zvan Diaconescu",
booktitle = {Recent Trends in Data Type Specification},
editor = {Magne Haveraaen and Olaf Owe and Ole-Johan Dahl},
publisher = "Springer",
series = "LNCS",
volume = 1130,
pages = {200--221},
year = 1996,
note = {Proceedings of 11th Workshop on Specification of Abstract Data
		  Types. Oslo, Norway, September 1995}}

@inproceedings{diacon96e,
title = "Foundations of Behavioral Specification in Rewriting Logic",
author = "R\u{a}zvan Diaconescu",
booktitle = "Proceedings, First International Workshop on Rewriting
  Logic and its Applications",
publisher = "Elsevier Science",
volume = 4,
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
note = "Asilomar, California",
year = 1996}

@InProceedings{diacon96f,
title = "Logical Semantics for \textsf{CafeOBJ}",
author = "R\u{a}zvan Diaconescu and Kokichi Futatsugi",
booktitle = "Precise Semantics for Software Modeling Techniques",
year = 1998,
publisher = "Proceedings of an ICSE'98 workshop held in Kyoto, Japan,
  published as Technical Report TUM-I9803, Technical University Munchen",
pages = "31--54",
note = "Preliminary version appeared as Technical Report
  IS-RR-96-0024S at Japan Advanced Institute for Science and
  Technology in 1996.  See {\small\tt
http://www4.informatik.tu-muenchen.de/\~{ }rumpe/icse98-ws/}"}

@misc{diacon96g,
title = "Constraint Logics",
author = "{R\u{a}zvan} Diaconescu",
year = 1996,
monthXXX = "December",
journal = "Mathematical Structures in Computer Science",
note= "Submitted for publication."}

@article{diacon96c,
title = "Category-based Modularization for Equational Logic Programming",
author = "R\u{a}zvan Diaconescu",
journal = "Acta Informatica",
volume = 33,
number = 5,
pages = "477--510",
year = 1996}

@article{diacon97,
title = "Extra Theory Morphisms in Institutions: logical semantics for
  multi-paradigm languages",
author = "R\u{a}zvan Diaconescu",
journal = "Applied Categorical Structures",
volume = 6,
number = 4,
pages = "427--453",
year = 1998}

@article{dia-beh,
title = "Behavioural coherence in object-oriented algebraic specification",
author = "R\u{a}zvan Diaconescu and K. Futatsugi",
journal = "Universal Computer Science",
volume = 6,
pages = "74--96",
year = 2000}

@phdthesis{diacon-thesis,
title = "Category-based Semantics for Equational and Constraint Logic
  Programming",
author = "R\u{a}zvan Diaconescu",
year = 1994,
school = "University of Oxford"}

@book{caferep98,
author = "R\u{a}zvan Diaconescu and Kokichi Futatsugi",
title = "{CafeOBJ} Report: The Language, Proof Techniques,
  and Methodologies for Object-Oriented Algebraic Specification",
year = 1998,
publisher = "World Scientific",
note = "AMAST Series in Computing, volume 6"}

@book{caferep98-fsh,
author = "R. Diaconescu and K. Futatsugi",
title = "{CafeOBJ} Report",
year = 1998,
publisher = "World Scientific",
note = "AMAST Series in Computing, volume 6"}

@article{diacon98a,
title = "Behavioral Coherence in Object-Oriented Algebraic Specification",
author = "R\u{a}zvan Diaconescu and Kokichi Futatsugi",
year = 2000,
journal = "Journal of Universal Computer Science",
volume = 6,
number = 1,
pages = "74--96",
note = "Also Japan Advanced Institute for Science and Technology
  Technical Report number IS--RR--98--0017F, 1998"}

@article{diacon98a-fsh,
title = "Behavioral Coherence in Object-Oriented Algebraic Specification",
author = "R. Diaconescu and K. Futatsugi",
year = 2000,
journal = "Journal of Universal Computer Science",
volume = 6,
number = 1,
pages = "74--96"}

@article{diacon98a-sh,
title = "Behavioral Coherence in Object-Oriented Algebraic Specification",
author = "R\u{a}zvan Diaconescu and Kokichi Futatsugi",
year = 2000,
journal = "Journal of Universal Computer Science",
volume = 6,
number = 1,
pages = "74--96"}

@TechReport{diacon98b,
author = "R\u{a}zvan Diaconescu and Petros Stefaneas",
title = "Categorical foundations of modularization for multi-paradigm
  languages",
institution = "Japan Advanced Institute for Science and Technology",
year = 1998,
number = "IS-RR-98-0014F"}

@article{diacon-futatsugi01,
author = "R\u{a}zvan Diaconescu and Kokichi Futatsugi",
title = "Logical Foundations of {CafeOBJ}",
journal = "Theor.\ Comput.\ Sci.",
volume = "304",
number = "1-2",
year = "2003, to appear"}

@misc{diacon-futatsugi99,
title = "Logical Foundations of {C}afe{OBJ}",
author = "R\u{a}zvan Diaconescu and Kokichi Futatsugi",
year = 1999,
note= "Submitted to Theor.\ Comput.\ Sci.."}

@article{dia-ult,
title = "Institution-independent
Ultraproducts",
author = "R\u{a}zvan Diaconescu",
journal = "Fundamenta Informaticae",
volume = 55,
number = "3-4",
pages = "321--348",
year = 2003}

@inproceedings{DBLP:conf/birthday/Diaconescu06,
  author    = {Razvan Diaconescu},
  title     = {Jewels of Institution-Independent Model Theory},
  booktitle = {Essays Dedicated to Joseph A. Goguen},
  year      = {2006},
  pages     = {65-98}
}

@article{dia-cra,
title = "An institution-independent proof of {Craig}
Interpolation Theorem",
author = "R\u{a}zvan Diaconescu",
journal = "Studia Logica",
volume = 77,
number=1,
pages = "59--79",
year = 2004}


@article{dijkstra66,
author = {Edsger Wybe Dijkstra},
title = {The Structure of the {THE} Multi-programming System},
journal = {Communications of the ACM},
volume = 9,
year = 1966}

@book{odonnell85,
title = "Equational Logic as a Programming Language",
author = "Michael O'Donnell",
publisher = "MIT",
year = 1985}

@book{dia-car,
author = "R\u{a}zvan Diaconescu",
title = "Institution-independent Model Theory",
publisher = "Springer",
year = 2008}

@inproceedings{drusinsky00,
author = "Doron Drusinsky",
title = "{The Temporal Rover and the ATG Rover}",
booktitle = "SPIN Model Checking and Software Verification",
series = "LNCS",
volume = 1885,
editor = "Klaus Havelund and John Penix and Willem Visser",
pages = "323--330",
publisher = "Springer",
year = 2000}

@inproceedings{duran-meseguer98,
author = "Francisco Dur\'an and Jos\'e Meseguer",
title = "An extensible module algebra for {Maude}",
booktitle = "Proceedings of the 2nd International Workshop on Rewriting Logic
  and its Applications",
editor = "Claude Kirchner and H{\' e}l{\` e}ne Kirchner",
year = 1998,
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
volume = 15,
publisher = "Elsevier"}

@inproceedings{duran-meseguer99,
author = {Francisco Dur\'an and Jos\'e Meseguer},
title = {Structured Theories and Institutions},
booktitle = "Proceedings of Category Theory and Computer Science 1999",
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
volume = 29,
publisher = "Elsevier",
year = 1999}

@inproceedings{duran-meseguer00,
author = "Francisco Dur\'an and Jos\'e Meseguer",
title = "On Parameterized Theories and Views in {Full Maude} 2.0",
booktitle = "Proceedings of the 3rd International Workshop on Rewriting Logic
  and its Applications",
editor = "Kokichi Futatsugi",
year = 2000,
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
volume = 36,
publisher = "Elsevier"}

@phdthesis{duran-thesis,
title = "A Reflective Module Algebra with Applications to the {Maude}
  Language",

author = "Francisco Dur\'an",
year = 1999,
school = "University of M\'alaga, Spain"}

@inproceedings{duran00,
author = "Francisco Dur\'an",
title = "The extensibility of {Maude}'s module algebra",
pages = "422--437",
editor = "Teodor Rus",
booktitle = "Proceedings of the 8th International Conference on Algebraic
  Methodology and Software Technology (AMAST'00)",
series = "LNCS",
publisher = "Springer Verlag",
year = "2000"}

@Unpublished{Duran00-tckbct,
  author =       {Francisco Dur{\'a}n},
  title =        {Termination checker and {K}nuth-{B}endix completion tools
                  for {Maude} equational specifications},
  year =         2000,
  note =         {Manuscript, Computer Science Laboratory, SRI
                  International, \url{http://maude.csl.sri.com/papers}}
}

@Unpublished{Duran00-ccct,
  author =       {Francisco Dur{\'a}n},
  title =        {Coherence checker and completion tools for {Maude}
                  specifications},
  year =         2000,
  note =         {Manuscript, Computer Science Laboratory, SRI
                  International, \url{http://maude.csl.sri.com/papers}}
}

@book{ehrig-mahr85,
Title = "Fundamentals of Algebraic Specification 1: Equations and
  Initial Semantics",
author = "Hartmut Ehrig and Bernd Mahr",
year = 1985,
publisher = "Springer",
note = "EATCS Monographs on Theor.\ Comput.\ Sci., Volume 6"}

@techreport{ehrig-orejas-corn-bald93,
author = "Hartmut Ehrig and Fernando Orejas and Felix Cornelius and Michael
  Baldamus",
title = "Abstract and Behaviour Module Specifications",
institution = "Technische Universit{\"a}t Berlin",
number = "Technical Report 93-25",
year = 1993}

@inproceedings{ehrig-baldamus-cornelius-orejas92,
author = "Hartmut Ehrig and Michael Baldamus and Felix Cornelius and
  Fernando Orejas",
title = "Theory of Algebraic Module Specification Including Behavioural
  Semantics and Constraints",
pages = "145--172",
editor = "Maurice Nivat and Charles Rattray and Teodor Rus and Giuseppe
  Scollo",
booktitle = "Proceedings of the Second International Conference on Algebraic
  Methodology and Software Technology",
monthXXX = may # "~22--25",
series = "Workshops in Computing",
publisher = "Springer Verlag",
address = "London",
year = "1992"}

@unpublished{elan,
author = "Peter Borovansk{\' y} and Hora{\c t}iu C{\^\i}rstea and
  Hubert Dubois and Claude Kirchner and H{\' e}l{\` e}ne Kirchner and
  Pierre-Etienne Moreau and Christophe Ringeissen and Marian Vittek",
title = "ELAN",
note = "User manual;
  {\footnotesize\url{http://www.loria.fr/equipes/protheo/SOFTWARES/ELAN}}"}

@unpublished{elan-fsh,
author = "P. Borovansk{\' y} and H. C{\^\i}rstea and
  H. Dubois and C. Kirchner and H. Kirchner and
  P.-E. Moreau and C. Ringeissen and M. Vittek",
title = "{ELAN}",
note = "User manual -- \url{http://www.loria.fr}"}

@inproceedings{chen-et-al03,
author = "Feng Chen and Grigore Ro\c{s}u and Ram prasad Venkatesan",
title = " Rule-Based Analysis of Dimensional Safety",
booktitle = "Rewriting Techniques and Applications (RTA'03)",
year = "2003",
series = "LNCS",
volume = 2706,
pages = "197--207",
publisher = "Springer"}

@article{DBLP:journals/jsc/Paulin-MohringW93,
  author    = {Christine Paulin-Mohring and
               Benjamin Werner},
  title     = {Synthesis of {ML} Programs in the System {C}oq},
  journal   = {J. Symb. Comput.},
  volume    = {15},
  number    = {5/6},
  year      = {1993},
  pages     = {607-640}
}

@incollection{fiadeiro-sernadas88,
author = "Jos\'e Fiadeiro and Amilcar Sernadas",
title = "Structuring Theories on Consequence",
booktitle = "Recent Trends in Data Type Specification",
editor = "Donald Sannella and Andrzej Tarlecki",
publisher = "Springer",
note = "LNCS, Volume 332",
year = 1988,
pages = "44--72"}

@inproceedings{DBLP:conf/types/BerghoferN00,
  author    = {Stefan Berghofer and
               Tobias Nipkow},
  title     = {Executing Higher Order Logic},
  booktitle = {TYPES},
  year      = {2000},
  pages     = {24-40}
}

@inproceedings{finkbeiner-et-al02,
title = "{Collecting Statistics over Runtime Executions}",
author = "Bernd Finkbeiner and Sriram Sankaranarayanan and Henny Sipma",
booktitle = {Proceedings of Runtime Verification (RV'02)},
publisher = "Elsevier Science",
editor = "Klaus Havelund and Grigore Ro\c{s}u",
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
year = "to appear, 2002"
}

@techreport{fischer-rosu01,
author = "Bernd Fischer and Grigore Ro\c{s}u",
title = "Interpreting Abstract Interpretations in Membership Equational
Logic",
year = "May 2001.  Written 23 February 2001",
institution = "RIACS",
number = "TR 01-16"}

@article{freyd-kelly72-sh,
author = "P. Freyd and G. Kelly",
title = "Categories of Continuous Functors",
year = "1972",
journal = "Journal of Pure and Applied Algebra",
volume = "2",
pages = "169--191",
}

@misc{ghani-luth-marchi-power01,
author = "Neil Ghani and Christoph Luth and Frederico de Marchi and
  John Power",
title = "Algebras, Coalgebras, Monads and Comonads"
}

@incollection{giannakopoulou-havelund01,
title = "{Automata-Based Verification of Temporal Properties on
  Running Programs}",
author = "Dimitra Giannakopoulou and Klaus Havelund",
booktitle = "Proceedings, International Conference on
  Automated Software Engineering (ASE'01)",
publisher = "Institute of Electrical and Electronics Engineers",
year = 2001,
pages = "412--416",
note = "Coronado Island, California"}

@incollection{montanari76,
title = "Observability Concepts in Abstract Data Specifications",
author = "V. Giarrantana and F. Gimona and Ugo Montanari",
booktitle = "Proceedings, Conference on Mathematical Foundations of
  Computer Science",
publisher = "Springer",
note = "LNCS, Volume 45",
year = 1976}

@incollection{montanari76-fsh,
title = "Observability Concepts in Abstract Data Specifications",
author = "V. Giarrantana and F. Gimona and U. Montanari",
booktitle = "Proceedings of MFCS",
publisher = "Springer",
series = "LNCS",
volume = 45,
year = 1976}

@book{gratzer71,
author = "George Gr{\"a}tzer",
title = "Lattice theory",
publisher = "W. H. Freeman and Company",
year = "1971",
address = "San Francisco"}

@techreport{gaudel-privara91,
author = "Marie-Claude Gaudel and Igor Privara",
title = "Context Induction: an Exercise",
institution = "LRI, Universit\'{e} de Paris-Sud",
number = "687",
year = 1991}

@techreport{gaudel-privara91-fsh,
author = "M.-C. Gaudel and I. Privara",
title = "Context Induction: an Exercise",
institution = "LRI, Universit\'{e} de Paris-Sud",
number = "687",
year = 1991}

@article{godel31,
author = "Kurt G{\"o}del",
title = "{\"U}ber formal unentscheidbare {S}{\"a}tze der
  {P}rincipia {M}athematica und verwandter {S}ystem {I}",
year = "1931",
journal = "Monatshefte f{\"u}r Mathematik und Physik",
volume = "32",
pages = "173--198",
}

@techreport{adj1,
title = "A Junction between Computer Science and Category Theory, {I}:
  Basic Concepts and Examples (Part 1)",
author = "Joseph Goguen and James Thatcher and Eric Wagner and Jesse
Wright",
year = 1973,
institution = "IBM Watson Research Center, Yorktown Heights NY",
note = "Report RC 4526"}

@techreport{adj2,
title = "A Junction between Computer Science and Category Theory, {I}:
  Basic Concepts and Examples (Part 2)",
author = "Joseph Goguen and James Thatcher and Eric Wagner and Jesse
Wright",
year = 1976,
institution = "IBM Watson Research Center, Yorktown Heights NY",
note = "Report RC 5908"}

@techreport{adj75,
title = "An Introduction to Categories, Algebraic Theories and Algebras",
author = "Joseph Goguen and James Thatcher and Eric Wagner and Jesse
Wright",
year = 1975,
institution = "IBM Watson Research Center, Yorktown Heights NY",
note = "Report RC 5369"}

@incollection{goguen75,
author = "Joseph Goguen",
title = "Semantics of Computation",
year = 1975,
booktitle = "Proceedings, First International Symposium on Category
  Theory Applied to Computation and Control",
editor = "Ernest Manes",
publisher = "Springer",
pages = "151--163",
note = "(San Fransisco, February 1974.)  LNCS,
  Volume 25"}

@incollection{gt74,
author = "Joseph Goguen and James Thatcher",
title = "Initial Algebra Semantics",
booktitle = "Proceedings, Fifteenth Symposium on Switching and Automata
  Theory",
pages = "63--77",
publisher = "Institute of Electrical and Electronics Engineers",
year = 1974}

@incollection{gtww75,
title = "Abstract Data Types as Initial Algebras and the Correctness of Data
  Representations",
author = "Joseph Goguen and James Thatcher and Eric Wagner and Jesse
Wright",
year = 1975,
booktitle = "Computer Graphics, Pattern Recognition and Data Structure",
editor = "Alan Klinger",
location = "Beverley Hills CA",
publisher = "Institute of Electrical and Electronics Engineers",
pages = "89--93"}

@incollection{goguen-thatcher-wagner76,
title = "An Initial Algebra Approach to the Specification, Correctness and
  Implementation of Abstract Data Types",
author = "Joseph Goguen and James Thatcher and Eric Wagner",
booktitle = "Current Trends in Programming Methodology, IV",
year = 1978,
publisher = "Prentice-Hall",
editor = "Raymond Yeh",
pages = "80--149"}

@article{gtww77,
author = "Joseph Goguen and James Thatcher and Eric Wagner and Jesse
Wright",
title = "Initial Algebra Semantics and Continuous Algebras",
journal = "Journal of the Association for Computing Machinery",
volume = 24, number = 1,
pages = "68--95",
monthXXX = "January",
year = 1977,
note = "An early version is ``Initial Algebra Semantics'', by Joseph Goguen
  and James Thatcher, IBM T. J. Watson Research Center, Report RC~4865, May
  1974"}

@article{gtww77-sh,
author = "Joseph Goguen and James Thatcher and Eric Wagner and Jesse
Wright",
title = "Initial Algebra Semantics and Continuous Algebras",
journal = "Journal of the Association for Computing Machinery",
volume = 24, number = 1,
pages = "68--95",
monthXXX = "January",
year = 1977}

@article{volSmi-probNon,
 author = {Volpano, Dennis and Smith, Geoffrey},
 title = {Probabilistic noninterference in a concurrent language},
 journal = {Journal of Computer Security},
 volume = {7},
 number = {2,3},
 year = {1999},
 pages = {231--253}
} 

@techreport{goguen78,
title = "Order Sorted Algebra",
author = "Joseph Goguen",
year = 1978,
number = "14",
institution = "UCLA Computer Science Department",
note = "Semantics and Theory of Computation Series"}

@book{denMarkov,
  author = {Kemeny, J. G. and Snell, J. L. and Knapp, A. W.},
  publisher = {Springer},
  title = {Denumerable {M}arkov chains (second edition)},
  year = 1976
}

@article{lump2,
title = "Bisimulation through probabilistic testing",
journal = "Information and Computation",
volume = "94",
number = "1",
pages = "1 - 28",
year = "1991",
author = "Kim G. Larsen and Arne Skou"
}

@incollection{goguen-meseguer82,
title = "Universal Realization, Persistent Interconnection and
  Implementation of Abstract Modules",
author = "Joseph Goguen and Jos\'e Meseguer",
year = 1982,
booktitle = "Proceedings, 9th International Conference on Automata,
Languages
  and Programming",
pages = "265--281",
editor = "M. Nielsen and E. M. Schmidt",
location = "Aarhus, Denmark",
publisher = "Springer",
note = "LNCS, Volume 140"}

@incollection{goguen-meseguer82-fsh,
title = "Universal Realization, Persistent Interconnection and
  Implementation of Abstract Modules",
author = "J. Goguen and J. Meseguer",
year = 1982,
booktitle = "ICALP",
pages = "265--281",
publisher = "Springer",
series = "LNCS",
volume = 140}

@article{osa1,
title = "Order-Sorted Algebra {I}: Equational Deduction for Multiple
  Inheritance, Overloading, Exceptions and Partial Operations",
author = "Joseph Goguen and Jos\'e Meseguer",
journal = "Theor.\ Comput.\ Sci.",
volume = 105,
number = 2,
pages = "217--273",
year = 1992}

@article{osa1-sh,
title = "Order-Sorted Algebra {I}: Equational Deduction for Multiple
  Inheritance, Overloading, Exceptions and Partial Operations",
author = "Joseph Goguen and Jos\'e Meseguer",
journal = "Theor.\ Comput.\ Sci.",
volume = 105, number = 2,
pages = "217--273",
year = 1992}

@article{osa1-fsh,
title = "Order-Sorted Algebra {I}: Equational Deduction for Multiple
  Inheritance, Overloading, Exceptions and Partial Operations",
author = "J. Goguen and J. Meseguer",
journal = "Theor.\ Comput.\ Sci.",
volume = 105, number = 2,
pages = "217--273",
year = 1992}

@article{solves93,
title = "Order-Sorted Algebra Solves the Constructor Selector, Multiple
  Representation and Coercion Problems",
author = "Jos\'e Meseguer and Joseph Goguen",
journal = "Information and Computation",
volume = 103, number = 1,
monthXXX = "March",
year = 1993,
pages = "114--158",
note = "Revision of a paper presented at LICS 1987"}

@incollection{goguen-tardo79,
title = "An Introduction to {OBJ}: A Language for Writing and Testing
Software
   Specifications",
author = "Joseph Goguen and Joseph Tardo",
year = 1979,
booktitle = "Specification of Reliable Software",
editor = "Marvin Zelkowitz",
publisher = "Institute of Electrical and Electronics Engineers",
location = "Cambridge MA",
pages = "170--189",
note = "Reprinted in {\it Software Specification Techniques\/}, Nehan Gehani
  and Andrew McGettrick, editors, Addison Wesley, 1985, pages 391--420"}

@article{goguen-burstall84a,
title = "Some Fundamental Algebraic Tools for the Semantics of Computation,
  Part 1: Comma Categories, Colimits, Signatures and Theories",
author = "Joseph Goguen and Rod Burstall",
year = 1984,
journal = "Theor.\ Comput.\ Sci.",
volume = 31, number = 2,
pages = "175--209"}

@article{goguen-burstall84b,
title = "Some Fundamental Algebraic Tools for the Semantics of Computation,
  Part 2: Signed and Abstract Theories",
author = "Joseph Goguen and Rod Burstall",
year = 1984,
journal = "Theor.\ Comput.\ Sci.",
volume = 31, number = 3,
pages = "263--295"}

@techreport{iida97,
author = "Shusaku Iida and Michihiro Matsumoto and R\u{a}zvan Diaconescu and
  Kokichi Futatsugi and Dorel Lucanu",
title = "Concurrent Object Composition in {CafeOBJ}",
year = 1997,
institution = "Japan Advanced Institute for Science and Technology",
number = "IS-RR-96-0024S"}

@incollection{ins1,
title = "Introducing Institutions",
author = "Joseph Goguen and Rod Burstall",
booktitle = "Proceedings, Logics of Programming Workshop",
editor = "Edmund Clarke and Dexter Kozen",
year = 1984,
location = "Carnegie-Mellon University",
publisher = "Springer",
note = "LNCS, Volume 164",
pages = "221--256"}

@techreport{ins2,
title = "Institutions: Abstract Model Theory for Computer Science",
author = "Joseph Goguen and Rod Burstall",
year = 1985,
institution = "Center for the Study of Language and Information,
  Stanford University", number = "CSLI-85-30"}

@incollection{goguen-burstall86,
title = "A Study in the Foundations of Programming Methodology:
  Specifications, Institutions, Charters and Parchments",
author = "Joseph Goguen and Rod Burstall",
booktitle = "Proceedings, Conference on Category Theory and Computer
  Programming",
editor = "David Pitt and Samson Abramsky and Axel Poign\'e and David
  Rydeheard",
location = "University of Surrey, Guildford, U.K.",
publisher = "Springer",
year = 1986,
pages = "313--333",
note = "LNCS, Volume 240"}

@article{goguen-meseguer85,
title = "Completeness of Many-sorted Equational Logic",
author = "Joseph Goguen and Jos\'e Meseguer",
year = 1985,
journal = "Houston Journal of Mathematics",
volume = 11, number = 3, pages = "307--334",
note = "Preliminary versions have appeared in: {\it SIGPLAN Notices}, July
  1981, Volume 16, Number 7, pages 24--37; SRI Computer Science Lab,
  Report CSL-135, May 1982; and Report CSLI-84-15, Center for the Study
  of Language and Information, Stanford University, September 1984"}

@article{goguen68,
title = "The Logic of Inexact Concepts",
author = "Joseph Goguen",
journal = "Synthese",
volume = 19,
year = "1968--69",
pages = "325--373"}

@incollection{goguen-parsaye81,
title = "Algebraic Denotational Semantics using Parameterized
  Abstract Modules",
author ="Joseph Goguen and Kamran Parsaye-Ghomi",
year = 1981,
booktitle = "Formalizing Programming Concepts",
location = "Peniscola, Spain",
editor = "J. Diaz and I. Ramos",
note = "LNCS, Volume 107",
pages = "292--309",
publisher = "Springer"}

@incollection{goguen-meseguer87,
title = "Unifying Functional, Object-Oriented and Relational Programming
  with Logical Semantics",
author = "Joseph Goguen and Jos\'{e} Meseguer",
booktitle = "Research Directions in Object-Oriented Programming",
editor = "Bruce Shriver and Peter Wegner",
year = 1987,
pages = "417--477",
publisher = "MIT Press"}

@incollection{tpasth,
title = "Types as Theories",
author = "Joseph Goguen",
booktitle = "Topology and Category Theory in Computer Science",
editor = "George Michael Reed and Andrew William Roscoe and Ralph F.
Wachter",
publisher = "Oxford",
year = 1991,
pages = "357--390",
note = "Proceedings of a Conference held at Oxford, June 1989"}

@incollection{tpasth-fsh,
title = "Types as Theories",
author = "J. Goguen",
booktitle = "Topology and Category Theory in Computer Science",
publisher = "Oxford",
year = 1991,
pages = "357--390"}

@incollection{tpasth-sh,
title = "Types as Theories",
author = "Joseph Goguen",
booktitle = "Topology and Category Theory in Computer Science",
editor = "George Michael Reed and Andrew William Roscoe and Ralph F.
Wachter",
publisher = "Oxford",
year = 1991,
pages = "357--390"}

@article{goguen91,
title = "A Categorical Manifesto",
author = "Joseph Goguen",
journal = "Mathematical Structures in Computer Science",
volume = 1,
number = 1,
monthXXX = "March",
year = 1991,
pages = "49--67"}

@inproceedings{tasop,
title = "Towards an Algebraic Semantics for the Object Paradigm",
author = "Joseph Goguen and R\u{a}zvan Diaconescu",
booktitle = "Proceedings, Tenth Workshop on Abstract Data Types",
editor = "Hartmut Ehrig and Fernando Orejas",
publisher = "Springer",
year =  1994,
pages = "1--29",
note = "LNCS, Volume 785"}

@inproceedings{tasop-fsh,
title = "Towards an Algebraic Semantics for the Object Paradigm",
author = "J. Goguen and R. Diaconescu",
booktitle = "Proceedings of WADT",
publisher = "Springer",
year =  1994,
series = "LNCS",
volume = 785}

@article{osa-survey,
title = "An {O}xford Survey of Order Sorted Algebra",
author = "Joseph Goguen and R\u{a}zvan Diaconescu",
journal = "Mathematical Structures in Computer Science",
volume = 4,
year = 1994,
pages = "363--392"}

@article{gog-ins,
title = "Institutions: Abstract Model Theory for Specification and
  Programming",
author = "Joseph Goguen and Rod Burstall",
journal = "Journal of the Association for Computing Machinery",
volume = 39,
number = 1,
year = 1992,
pages = "95--146"}

@article{ins-sh,
title = "Institutions: Abstract Model Theory for Specification and
  Programming",
author = "Joseph Goguen and Rod Burstall",
journal = "Journal of the Association for Computing Machinery",
volume = 39,
number = 1,
year = 1992,
monthXXX = "January",
pages = "95--146"}

@article{ins-fsh,
title = "Institutions: Abstract Model Theory for Specification and
  Programming",
author = "J. Goguen and R. Burstall",
journal = "Journal of the ACM",
volume = 39,
number = 1,
year = 1992,
monthXXX = "January",
pages = "95--146"}

@incollection{gmal94,
title = "Proof of Correctness of Object Representation",
author = "Joseph Goguen and Grant Malcolm",
booktitle = "A Classical Mind: Essays in Honour of C. A. R.~Hoare",
editor = "A. William Roscoe",
publisher = "Prentice-Hall",
pages = "119--142",
year = 1994}

@incollection{goguen-tracz00,
author = "Joseph Goguen and William Tracz",
booktitle = "Foundations of Component-based Systems",
editor = "Gary Leavens and Murali Sitaraman",
title = "An Implementation-Oriented Semantics for Module Composition",
year = "2000",
pages = "231--263",
publisher = "Cambridge"}

@book{goguen-malcolm96,
title = "Algebraic Semantics of Imperative Programs",
author= "Joseph Goguen and Grant Malcolm",
publisher = "MIT",
year = 1996}

@book{goguen-malcolm96-fsh,
title = "\mbox{Algebraic Semantics of Imperative Programs. {\em MIT, 1996}}",
author= "J. Goguen and G. Malcolm"}

@article(ha-sh,
author = "Joseph Goguen and Grant Malcolm",
title = "A Hidden Agenda",
journal = "Theor.\ Comput.\ Sci.",
volume = 245,
number = 1,
pages = "55--101",
year = "August 2000")

@article{ha-fsh,
author = "J. Goguen and G. Malcolm",
title = "A Hidden Agenda",
journal = "J. of TCS",
volume = 245,
number = 1,
pages = "55--101",
year = "2000"}

@article{goguen-malcolm99,
author = "Joseph Goguen and Grant Malcolm",
title = "A Hidden Agenda",
journal = "Theor.\ Comput.\ Sci.",
note = "Also UCSD Dept.\ Computer Science \& Eng.\ Technical Report
  CS97--538, May 1997",
year = "to appear"}

@article{goguen-malcolm99a,
author = "Joseph Goguen and Grant Malcolm",
title = "Hidden Coinduction: Behavioral correctness proofs for objects",
journal = "Mathematical Structures in Computer Science",
volume = 9,
number = 3,
pages = "287--319",
year = "1999"}

@article{goguen-malcolm99a-fsh,
author = "J. Goguen and G. Malcolm",
title = "Hidden Coinduction: Behavioral correctness proofs for objects",
journal = "Mathematical Structures in Computer Science",
volume = 9,
number = 3,
pages = "287--319",
year = "1999"}

@incollection{habs,
title = "Extended Abstract of a Hidden Agenda",
author = "Joseph Goguen and Grant Malcolm",
booktitle = "Proceedings, Conference on Intelligent Systems: A
  Semiotic Perspective",
editor = "James Albus and Alex Meystel and Richard Quintero",
publisher = "National Inst.\ Standards and Technology",
year = 1996,
note = "Gaithersberg MD, October 20--23",
pages = "159--167"}

@incollection{cafe98,
title = "Tools for Distributed Cooperative Design and Validation",
author = "Joseph Goguen and Kai Lin and Akira Mori and Grigore Ro\c{s}u and
  Akiyoshi Sato",
booktitle = "Proceedings, CafeOBJ Symposium",
publisher = "Japan Advanced Institute for Science and Technology",
year = 1998,
note = "Numazu, Japan, April 1998"}

@incollection{ase97,
title = "Distributed Cooperative Formal Methods Tools",
author = "Joseph Goguen and Kai Lin and Akira Mori and Grigore Ro\c{s}u and
  Akiyoshi Sato",
booktitle = "Proceedings, International Conference on
  Automated Software Engineering (ASE'97)",
publisher = "Institute of Electrical and Electronics Engineers",
year = 1997,
note = "Lake Tahoe, Nevada, 3-5 November 1997",
pages = "55--62"}

@incollection{goguen97,
author = "Joseph Goguen",
title = "Stretching First order Equational Logic:
  Proofs with Partiality, Subtypes and Retracts",
editor = "Maria Paola Bonacina and Ulrich Furbach",
booktitle = "Proceedings, Workshop on First Order Theorem Proving",
pages = "78--85",
year = 1997,
note = "Schloss Hagenberg, Austria, October 1997; RISC-Linz Report No.\
  95--50; revised version with appendixes co-authored with Grigore Ro\c{s}u
  to appear in {\em Journal of Symbolic Computation}"}

@incollection{tat99,
title = "An Overview of the {T}atami Project",
author = "Joseph Goguen and Kai Lin and Grigore Ro\c{s}u and Akira Mori and
  Bogdan Warinschi",
booktitle = "Cafe: An Industrial-Strength Algebraic Formal Method",
editor = "Kokichi Futatsugi and Ataru Nakagawa and Tetsuo Tamai",
publisher = "Elsevier",
pages = "61--78",
year = "2000"}

@incollection{goguen-lin-rosu-mori-warinschi00,
title = "An Overview of the {T}atami Project",
author = "Joseph Goguen and Kai Lin and Grigore Ro\c{s}u and Akira Mori and
  Bogdan Warinschi",
booktitle = "Cafe: An Industrial-Strength Algebraic Formal Method",
editor = "Kokichi Futatsugi and Ataru Nakagawa and Tetsuo Tamai",
publisher = "Elsevier",
pages = "61--78",
year = "2000"}

@book{tp,
title = "Theorem Proving and Algebra",
author = "Joseph Goguen",
year = "to appear",
publisher = "MIT"}

@incollection{goguen-rosu99,
title = "Hiding More of Hidden Algebra",
author = "Joseph Goguen and Grigore Ro\c{s}u",
booktitle = "Formal Methods 1999 (FM'99)",
series = "LNCSs",
volume = "1709",
publisher = "Springer",
pages = "1704--1719",
year = 1999}

@incollection{goguen-rosu99-fsh,
title = "Hiding More of Hidden Algebra",
author = "J. Goguen and G. Ro\c{s}u",
booktitle = "Proceeding of FM'99",
series = "LNCS",
volume = "1709",
publisher = "Springer",
pages = "1704--1719",
year = 1999}

@inproceedings{goguen-rosu99b,
title = "A Protocol for Distributed Cooperative Work",
author = "Joseph Goguen and Grigore Ro\c{s}u",
booktitle = {Proceedings of Workshop on Distributed Systems 1999
  (WDS'99), Iasi, Romania, 2 September 1999},
publisher = "Elsevier Science",
volume = 28, pages = "1--22",
editor = "Gheorghe \c{S}tef\u{a}nescu",
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
year = 1999}

@inproceedings{goguen99,
title = "An Introduction to Algebraic Semiotics, with Applications to User
  Interface Design",
author = "Joseph Goguen",
booktitle = {Computation for Metaphors, Analogy and Agents},
publisher = "Springer",
volume = 1562,
editor = "Chrystopher Nehaniv",
series = "Lecture Notes in Artificial Inteligence",
pages = "242--291",
year = 1999}

@incollection{iobj,
author = "Joseph Goguen and Timothy Winkler and {Jos\'e} Meseguer and
  Kokichi Futatsugi and Jean-Pierre Jouannaud",
title = "Introducing {OBJ}",
booktitle = "Software Engineering with {OBJ}: algebraic specification in
  action",
editor = "Joseph Goguen and Grant Malcolm",
year = "2000", pages = "3--167",
publisher = "Kluwer"}

@incollection{iobj-fsh,
author = "J. Goguen and T. Winkler and J. Meseguer and
  K. Futatsugi and J.-P. Jouannaud",
title = "Introducing {OBJ}",
booktitle = "Software Engineering with {OBJ}: algebraic specification in
  action",
year = "2000",
pages = "3--167",
publisher = "Kluwer"}

@inproceedings(goguen-lin-rosu00,
title = "Circular Coinductive Rewriting",
author = "Joseph Goguen and Kai Lin and Grigore Ro\c{s}u",
booktitle = "Proceedings, Automated Software Engineering '00",
publisher = "IEEE",
pages = "123--131",
note = "(Grenoble, France)",
year = 2000)

@inproceedings{circularCoinduction1,
title = "Circular Coinductive Rewriting",
author = "J. Goguen and K. Lin and G. Ro\c{s}u",
booktitle = "Proceedings of Automated Software Engineering '00",
publisher = "IEEE",
pages = "123--131",
year = 2000}


@article{goldblatt01,
author = "Robert Goldblatt",
title = "What is the Coalgebraic Analogue of Birkhoff's Variety Theorem?",
journal = "Theor.\ Comput.\ Sci.",
year = "to appear"}

@inproceedings{goguen-lin-rosu00b,
title = "Behavioral and Coinductive Rewriting",
author = "Joseph Goguen and Kai Lin and Grigore Ro\c{s}u",
booktitle = "Proceedings of the 3rd International Workshop on Rewriting Logic
  and its Applications",
editor = "Kokichi Futatsugi",
year = 2000,
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
volume = 36,
pages = "1--22",
publisher = "Elsevier"}

@incollection{goguen-lin-rosu00b-fsh,
title = "Behavioral and Coinductive Rewriting",
author = "J. Goguen and K. Lin and G. Ro\c{s}u",
booktitle = "Proceedings of WRLA'01",
publisher = "Elsevier",
year = "2001",
series = "ENTCS",
volume = "36",
pages = "1--22"}

@article{goguen-malcolm-kemp98,
author = "Joseph Goguen and Grant Malcolm and Tom Kemp",
title = "A Hidden {Herbrand} Theorem: Combining the Object, Logic and
  Functional Paradigms",
journal = "LNCS",
volume = "1490",
pages = "445--462",
year = "1998"}

@incollection{goguen-malcolm-kemp98-fsh,
author = "J. Goguen and G. Malcolm and T. Kemp",
title = "A Hidden {Herbrand} Theorem: Combining the Object, Logic and
  Functional Paradigms",
booktitle = "Proceedings of PLIP/ALP'98",
publisher = "Springer",
series = "LNCS",
volume = "1490",
pages = "445--462",
year = "1998"}

@article{goguen00,
author = "Joseph Goguen",
title = "Hidden Algebra and Concurrent Distributed Software",
journal = "Software Engineering Notes",
volume = "25",
number = "1",
year = "2000"}

@article{goguen-rosu02,
author = "Joseph Goguen and Grigore Ro\c{s}u",
title = "Institution Morphisms",
journal = "Formal Aspects of Computing",
volume = 13,
number = "3-5",
pages = "274--307",
year = "2002"}

@article{goguen-rosu02-fsh,
author = "J. Goguen and G. Ro\c{s}u",
title = "Institution Morphisms",
journal = "Formal Aspects of Computing",
volume = 13,
number = "3-5",
pages = "274--307",
year = "2002"}

@article{gordon95,
author = "Andrew Gordon",
title = "Bisimilarity as a theory of functional programming",
journal = "Electr.\ Notes Theor.\ Comput.\ Sci.",
volume = 1,
year = 1995}

@article{groote-vaandrager92-fsh,
author = "J. F. Groote and F. W. Vaandrager",
title = "Structured Operational Semantics and Bisimulation as a Congruence",
journal = "Information and Computation",
volume = "100",
number = "2",
pages = "202--260",
year = 1992}

@article{grothendieck57,
title = "Sur quelques points d'alg\'ebre homologique",
author = "Alexandre Grothendieck",
journal = "T\^ohoku Mathematical Journal",
volume = 2,
pages = "119--221",
year = 1957}

@inproceedings{gumm98,
title = "Equational and Implicational Classes of Coalgebras.
  Extended Abstract.",
author = "H. Peter Gumm",
booktitle = {The 4th International Seminar on Relational Methods in Logic,
  Algebra and Computer Science.},
note = "Warsaw",
year = 1998}

@inproceedings{gumm-schroder98,
title = "Covarieties and Complete Covarieties",
author = {H. Peter Gumm and Tobias Schr\"oder},
booktitle = {Proceedings of the First Workshop on Coalgebraic Methods
  in Computer Science (CMCS'98), Lisbon, Portugal, March 1998},
publisher = "Elsevier Science",
pages = "43--56",
volume = 11,
editor = "Bart Jacobs and Larry Moss and Horst Reichel and Jan Rutten",
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
year = 1998}

@incollection{hagino87,
author = "Tatsuya Hagino",

title = "A Typed Lambda Calculus with Categorical Type Constructors",
editor = "D. H. Pitt and A. Poign{\'e} and D. E. Rydeheard",
booktitle = "Proceedings 2nd Int.\ Conf.\ on Category Theory and Computer
  Science, CTCS'87, Edinburgh, UK, 7--9 Sept 1987",
series = "LNCS",
volume = "283",
pages = "140--157",
publisher = "Springer",
address = "Berlin",
year = "1987"}

@phdthesis{hamel-thesis,
title =  "Behavioural Verification and Implementation of an Optimizing
  Compiler for {OBJ3}",
author = "Lutz Hamel",
school = "University of Oxford",
year = 1996}

@inproceedings{hamel-rosu02,
title = "Towards Behavioral Compiler Correctness Proofs using Hidden Logic",
author = "Lutz Hamel and Grigore Ro{\c s}u",
note = "Submitted for publication",
year = 2002}

@phdthesis{hamel-thesis-fsh,
title =  "Behavioural Verification and Implementation of an Optimizing
  Compiler for {OBJ3}",
author = "L. Hamel",
school = "University of Oxford",
year = 1996}

@article{havelund-lowry-penix98,
author = "Klaus Havelund and Michael Lowry and John Penix",
title = "{Formal Analysis of a Space Craft Controller using SPIN}",
journal = "IEEE Transactions on Software Engineering",
monthXXX = aug,
year = 2001,
volume = 27,
number = 8,
pages = "749--765"}

@article{havelund-pressburger00,
author = "Klaus Havelund and Thomas Pressburger",
title = "{Model Checking Java Programs using Java PathFinder}",
journal = "International Journal on Software Tools for Technology Transfer",
monthXXX = apr,
year = 2000,
volume = 2,
number = 4,
pages = "366--381",
note = "Special issue of STTT containing selected submissions to the
  4th SPIN workshop, Paris, France, 1998"}

@inproceedings{havelund-rosu01,
author = "Klaus Havelund and Grigore Ro\c{s}u",
title = "{Java PathExplorer -- {A} Runtime Verification Tool}",
booktitle = "The 6th International Symposium on Artificial Intelligence,
  Robotics and Automation in Space: A New Space Odyssey",
address = "Montreal, Canada, June 18--21",
year = "2001"}

@INPROCEEDINGS{smi-NewTypeSys,
author={Smith, Geoffrey},
booktitle={CSFW},
title={A new type system for secure information flow},
year={2001},
pages={115--125}
}

@inproceedings{havelund-johnson-rosu01a,
author = "Klaus Havelund and Scott Johnson and Grigore Ro\c{s}u",
title = "{Specification and Error Pattern Based Program Monitoring}",
booktitle = "European Space Agency Workshop on On-Board Autonomy",
address = "Noordwijk, The Netherlands",
year = "2001"}

@incollection{havelund-rosu01b,
title = "{Monitoring Programs using Rewriting}",
author = "Klaus Havelund and Grigore Ro\c{s}u",
booktitle = "Proceedings, International Conference on
  Automated Software Engineering (ASE'01)",
publisher = "Institute of Electrical and Electronics Engineers",
year = 2001,
pages = "135--143",
note = "Coronado Island, California"}

@inproceedings{havelund-rosu01c,
title = "{Monitoring Java Programs with Java PathExplorer}",
author = "Klaus Havelund and Grigore Ro\c{s}u",
booktitle = {Proceedings of Runtime Verification (RV'01)},
publisher = "Elsevier Science",
editor = "Klaus Havelund and Grigore Ro\c{s}u",
volume = 55,
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
year = 2001}

@book{havelund-rosu01d,
title = "Runtime Verification 2001",
author = "Klaus Havelund and Grigore Ro\c{s}u",
publisher = "Elsevier Science",
volume = 55,
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
note = "Proceedings of a {\em Computer Aided Verification (CAV'01)}
  satellite workshop",
year = 2001}

@book{havelund-rosu02b,
title = "Runtime Verification 2002",
author = "Klaus Havelund and Grigore Ro\c{s}u",
publisher = "Elsevier Science",
volume = 70,
number = 4,
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
note = "Proceedings of a {\em Computer Aided Verification (CAV'02)}
  satellite workshop",
year = 2002}

@inproceedings{havelund-rosu02,
title = "Synthesizing Monitors for Safety Properties",
author = "Klaus Havelund and Grigore Ro{\c s}u",
booktitle = {Tools and Algorithms for Construction and Analysis of Systems
  (TACAS'02)},
publisher = "Springer",
series = "LNCS",
volume = 2280,
pages = "342--356",
note = "EASST best paper award at ETAPS'02",
year = 2002}

@inproceedings{havelund-shankar96,
author = "Klaus Havelund and Natarajan Shankar",
title = "{Experiments in Theorem Proving and Model Checking for
  Protocol Verification}",
booktitle = "FME'96: Industrial Benefit and Advances in Formal Methods",
series = "LNCS",
volume = 1051,
year = 1996,
editor = "Marie Claude Gaudel and Jim Woodcock",
pages = "662--681",
publisher = "Springer"}

@article{hennicker91,
title = "Context Induction: a Proof Principle for Behavioral Abstractions",
author = "Rolf Hennicker",
journal = "Formal Aspects of Computing",
volume = 3,
number = 4,
pages = "326--345",
year = 1991}

@article{hennicker91-fsh,
title = "Context Induction: a Proof Principle for Behavioral Abstractions",
author = "R. Hennicker",
journal = "Formal Aspects of Computing",
volume = 3,
number = 4,
pages = "326--345",
year = 1991}

@inproceedings{hennicker-kurz99,
title = "On the Algebraic Extension of Coalgebraic Specifications",
author = "Rolf Hennicker and Alexander Kurz",
booktitle = {Proceedings of the Second Workshop on Coalgebraic Methods
  in Computer Science (CMCS'99), Amsterdam, The Netherlands, March 1999},
publisher = "Elsevier Science",
volume = 19,
editor = "Bart Jacobs and Jan Rutten",
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
year = 1999}

@inproceedings{hennicker-bidoit99,
title = "Observational Logic",
author = "Rolf Hennicker and Michel Bidoit",
booktitle = {Algebraic Methodology and Software Technology (AMAST'98)},
publisher = "Springer",
series = "LNCS",
volume = 1548,
pages = "263--277",
year = 1999}

@inproceedings{hennicker-bidoit99-fsh,
title = "Observational Logic",
author = "R. Hennicker and M. Bidoit",
booktitle = "Proceedings of AMAST'98",
publisher = "Springer",
series = "LNCS",
volume = 1548,
pages = "263--277",
year = 1999}

@book{herrlich-strecker73,
title = "Category Theory",
author = "Horst Herrlich and George Strecker",
year = 1973,
publisher = "Allyn and Bacon"}

@article{hermida-StructIndCoind,
  author    = {Claudio Hermida and
               Bart Jacobs},
  title     = {Structural Induction and Coinduction in a Fibrational Setting},
  journal   = {Inf. Comput.},
  volume    = {145},
  number    = {2},
  year      = {1998},
  pages     = {107--152},
  ee        = {https://doi.org/10.1006/inco.1998.2725},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{hensel-interatedRecursion,
  author    = {Ulrich Hensel and
               Bart Jacobs},
  title     = {Proof Principles for Datatypes with Iterated Recursion},
  booktitle = {Category Theory and Computer Science},
  year      = {1997},
  pages     = {220--241}
}

@inproceedings{hensel-reichel95,
title = "Defining Equations in Terminal Coalgebras",
author = "Ulrich Hensel and Horst Reichel",
booktitle = {Recent Trends in Data Type Specification},
editor = {Egidio Astesiano and Gianna Reggio and Andrzej Tarlecki},
publisher = "Springer",
series = "LNCS",
volume = 906,
pages = {307--318},
year = 1995}

@misc{hilberdink-inclusions,
title = "Inclusion Systems",
author = "Hendrik Hilberdink",
school = "University of Oxford",
note = "Unpublished paper",
year = 1996}

@book{hindley-seldin86,
author = "J. Roger Hindley and Jonathan P. Seldin",
title = "Introduction to Combinatory Logic and Lambda Calculus",
publisher = "Cambridge University Press",
year = "1986"}

@article{hintermeier-et-al98,
author = "Claus Hintermeier and Claude Kirchner and H{\' e}l{\`e}ne
Kirchner",
title = "Dynamically-Typed Computations for Order-Sorted Equational
  Presentations",
journal = "Journal of Symbolic Computation",
monthXXX = apr,
number = 4,
pages = "455--526",
volume = 25,
year = 1998}

@article{hintermeier-et-al98-sh,
author = "C. Hintermeier and C. Kirchner and H. Kirchner",
title = "Dynamically-Typed Computations for Order-Sorted Equational
  Presentations",
journal = "Journal of Symbolic Computation",
monthXXX = apr,
number = 4,
pages = "455--526",
volume = 25,
year = 1998}

@inproceedings{hoare-et-al90-fsh,
author = "C. A. R. Hoare and H. Jifeng and J. P. Bowen and P. K. Pandya",
title = "An Algebraic Approach to Verifiable Compiling Specification and Prototyping of the {ProCoS} Level 0 Programming Language",
booktitle = "Proceedings of ESPRIT'90",
publisher = "Kluwer",
pages = "804--818",
year = "1990"}

@inproceedings{holzmann-smith99,
author      = "Gerard J. Holzmann and Margaret H. Smith",
title       = "{A Practical Method for Verifying Event-Driven Software}",
booktitle   = "Proceedings of ICSE'99, International Conference
  on Software Engineering",
address = "Los Angeles, California, USA",
publisher   = "IEEE/ACM",
year        = 1999,
month       = may}

@phdthesis{hsiang81,
title = "Refutational Theorem Proving using Term Rewriting Systems",
author = "Jieh Hsiang",
year = 1981,
school = "University of Illinois at Champaign-Urbana"}

@article{huet77,
title = "Confluent Reductions: Abstract Properties and Applications to Term
  Rewriting Systems",
author = "G\'erard Huet",
journal = "Journal of the Association for Computing Machinery",
year = 1980,
volume = 27, number = 4,
pages = "797--821",
note = "Preliminary version in {\it Proceedings}, 18th IEEE Symposium on
  Foundations of Computer Science, IEEE, 1977, pages 30--45"}

@article{huet80-fsh,
title = "Confluent Reductions: Abstract Properties and Applications to Term
  Rewriting Systems",
author = "G. Huet",
journal = "Journal of the Association for Computing Machinery",
year = 1980,
volume = 27, number = 4,
pages = "797--821"}

@unpublished{BOBJ,
title = "{BOBJ}",
note = "http://cseweb.ucsd.edu/groups/tatami/bobj"}

@article{isbell64,
title = "Subobjects, adequacy, completeness and categories of algebras",
author = "J. R. Isbell",
journal = "Rozprawy Matematyczne",
volume = 36,
pages = "1--33",
year = 1964}

@incollection{jacobs95,
author = "Bart Jacobs",
title = "Mongruences and Cofree Coalgebras",
booktitle = "Algebraic Methodology and Software Technology (AMAST95)",
editor = "Maurice Nivat",
publisher = "Springer",
note = "LNCS, Volume 936",
pages = "245--260",
year = 1995}

@incollection{jacobs96,
author = "Bart Jacobs",
title = "Objects and Classes, Coalgebraically",
booktitle = "Object-Orientation with Parallelism and Persistence",
editor = "B.\ Freitag and Cliff Jones and C.\ Lengauer and H.-J.\ Schek",
pages = "83--103",
publisher = "Kluwer",
year = 1996}

@inproceedings{jacobs96a,
author = "Bart Jacobs",
title = "Inheritance and cofree constructions",
booktitle = "Proceedings of ECOOP'96",
year = "1996",
pages = "210--231",
publisher = "Springer",
series = "LNCS",
volume = 1098}

@article{jacobs-rutten97,
title = "A Tutorial on (Co)Algebras and (Co)Induction",
author = "Bart Jacobs and Jan Rutten",
journal = "Bulletin of the European Association for Theoretical Computer
  Science",
volume = 62,
year = 1997,
pages = "222--259"}

@article{jacobs-rutten97-fsh,
title = "A Tutorial on (Co)Algebras and (Co)Induction",
author = "B. Jacobs and J. Rutten",
journal = "Bulletin of the European Association for Theoretical Computer
  Science",
volume = 62,
year = 1997,
pages = "222--259"}

@techreport{jacobs97,
author = "Bart Jacobs",
title = "Invariants, bisimulations and the correctness of Coalgebraic
  Refinements",
institution = "Computer Science Institute, Nijmegen",
number = "CSI-R9704",
year = 1997}

@misc{jacobs99,
author = "B. Jacobs",
title = "Coalgebras in specification and verification for object-oriented
  languages",
year = "1999"
}

@misc{jtrek,
author = "JTrek",
title  = "Web Page",
note = "{\small{\tt http://www.compaq.com/java/download}}"}

@misc{javacc,
author = "JavaCC",
title  = "Web Page",
note = "{\small{\tt http://www.webgain.com/products/java\_cc}}"}

@inproceedings{kamin80,
author = "Samuel Kamin",
title = "Final Data Type Specifications: {A} New Data Type Specification
  Method",
booktitle = "Conference Record of the Seventh Annual {ACM} Symposium on
  Principles of Programming Languages",
year = "1980",
organization = "ACM SIGACT and SIGPLAN",
publisher = "ACM",
pages = "131--138"}

@incollection{kaphengst-reichel77,
author = "H. Kaphengst and Horst Reichel",
title = "Initial Algebraic Semantics for Non-Context-Free Languages",
year = 1977,
booktitle = "Fundamentals of Computation Theory",
editor = "Marek Karpinski",
series = "LNCS",
volume = 56,
publisher = "Springer",
pages = "120--126"}

@incollection{kaphengst-reichel77-sh,
author = "H. Kaphengst and H. Reichel",
title = "Initial Algebraic Semantics for Non-Context-Free Languages",
year = 1977,
booktitle = "Fundamentals of Computation Theory",
editor = "M. Karpinski",
series = "LNCS",
volume = 56,
publisher = "Springer",
pages = "120--126"}

@article{kreowski-mossakowski95,
title = "Equivalence and difference between institutions:
  simulating {Horn} {Clause} {Logic} with based algebras",
author = "{Hans-J{\"o}rg} Kreowski and Till Mossakowski",
pages = "189--215",
journal = "Mathematical Structures in Computer Science",
monthXXX = jun,
year = "1995",
volume = "5",
number = "2"}

@inproceedings{kurz98,
author = "Alexander Kurz",
title = "A Co-Variety-Theorem for Modal Logic",
booktitle = "Proceedings of Advances in Modal Logic, Uppsala",
year = "1998",
publisher = "CSLI Stanford"}

@article{kurz-hennicker00,
author = "Alexander Kurz and Rolf Hennicker",
title = "On Institutions for Modular Coalgebraic Specifications",
journal = "Theor.\ Comput.\ Sci.",
year = "to appear"}

@misc{kurz-pattinson00,
author = "Alexander Kurz and Dirk Pattinson",
title = "Coalgebras and Modal Logic for Parameterised Endofunctors"}

@inproceedings{kurz98-fsh,
title = "Specifying Coalgebras with Modal Logic",
author = "A. Kurz",
booktitle = "Proceedings of CMCS'98",
publisher = "Elsevier",
volume = 11,
series = "ENTCS",
year = 1998}

@book{lambek66,
author = "Joachim Lambek",
title = "Completions of Categories",
year = 1966,
publisher = "Springer",
note = "Lecture Notes in Mathematics, Volume 24"}

@book{lambek-scott86,
title = "Introduction to Higher Order Categorical Logic",
author = "Joachim Lambek and Phil Scott",
publisher = "Cambridge",
year = 1986,
note = "Cambridge Studies in Advanced Mathematics, Volume 7"}

@inproceedings{lee-et-al99,
author = "Insup Lee and Sampath Kannan and Moonjoo Kim and Oleg Sokolsky and
  Mahesh Viswanathan",
title = "{Runtime Assurance Based on Formal Specifications}",
booktitle = "Proceedings of the International Conference on Parallel
  and Distributed Processing Techniques and Applications",
year = 1999}

@phdthesis{levy-thesis,
author = "B. Levy",
title =	"An Approach to Compiler Correctness Using Interpretation
  Between Theories",
school = "Computer Science Laboratory, The Aerospace Corporation",
year = "1986",
address = "El Segundo, CA",
monthXXX =	"December"}

@phdthesis{levy-thesis-fsh,
author = "B. Levy",
title =	"An Approach to Compiler Correctness Using Interpretation
  Between Theories",
school = "Comp. Sci. Lab., Aerospace Corporation",
year = "1986",
address = "El Segundo, CA"}

@article{los49,
title = "O matrycach logicznych",
author = "J. {\L}os",
journal = "Travaux de la Soci{\' e}t{\' e} des Sciences et Lettres de
  Wroc{\l}aw",
note = "Seria B, Nr. 19, Wroc{\l}aw",
year = 1949}

@incollection{lpr01,
title = "Certifying Domain-Specific Policies",
author = "Michael Lowry and Thomas Pressburger and Grigore Ro\c{s}u",
booktitle = "Proceedings, International Conference on
  Automated Software Engineering (ASE'01)",
publisher = "IEEE",
year = 2001,
pages = "81--90",
note = "Coronado Island, California"}

@incollection{lpr01-fsh,
title = "Certifying Domain-Specific Policies",
author = "M. Lowry and T. Pressburger and G. Ro\c{s}u",
booktitle = "Proceedings, International Conference on
  Automated Software Engineering (ASE'01)",
publisher = "IEEE",
year = 2001,
pages = "81--90",
note = "San Diego, California"}

@inproceedings{lucanu99,
title = "Bisimulation and Hidden Algebra",
author = "Dorel Lucanu and Ovidiu Gheorghie\c{s} and Adriana Apetrei",
booktitle = {Proceedings of the Second Workshop on Coalgebraic Methods
  in Computer Science (CMCS'99), Amsterdam, The Netherlands, March 1999},
pages = "213--232",
editor = "Bart Jacobs and Jan Rutten",
publisher = "Elsevier Science",
volume = 19,
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
year = 1999}

@inproceedings{lucanu99-fsh,
title = "Bisimulation and Hidden Algebra",
author = "D. Lucanu and O. Gheorghie\c{s} and A. Apetrei",
booktitle = "Proceedings of CMCS'99",
pages = "213--232",
publisher = "Elsevier",
volume = 19,
series = "ENTCS",
year = 1999}

@incollection{lucanu99a,
title = "Algebraic Specification of Object Aggregation",
author = "Dorel Lucanu",
editor = "Kokichi Futatsugi and Joseph Goguen and Jos{\' e} Meseguer",
booktitle = "OBJ/CafeOBJ/Maude at Formal Methods '99",
publisher = "Theta",
note = "Proceedings of a workshop held in Toulouse, France,
  20th and 22nd September 1999",
year = 1999,
pages = "115--132"}

@book{mac-cat,
title = "Categories for the Working Mathematician",
author = "Saunders Mac{\ }Lane",
year = 1971,
publisher = "Springer"}

@article{majster77,
title = "Limits of the Algebraic Specification of Abstract Data Types",
author = "Mila Majster",
journal = "SIGPLAN Notices ",
year = 1977,
monthXXX = "October",
pages = "37--42"}

@article{majster77-fsh,
title = "Limits of the Algebraic Specification of Abstract Data Types",
author = "M. Majster",
journal = "SIGPLAN Notices ",
year = 1977,
monthXXX = "October",
pages = "37--42"}

@article{malcolm90,
author = "Grant Malcolm",
title = "Data Structures and Program Transformation",
journal = "Science of Computer Programming",
volume = "14",
pages = "255--279",
year = "1990"}

@techreport{malg94,
title = "Proving Correctness of Refinement and Implementation",
author = "Grant Malcolm and Joseph Goguen",
institution = "Programming Research Group, University of Oxford",
number = "Technical Monograph PRG-114",
year = 1994}

@incollection{malcolm96,
author = "Grant Malcolm",
title = "Behavioural equivalence, bisimilarity, and minimal realisation",
editor = "Magne Haveraaen and Olaf Owe and Ole-Johan Dahl",
booktitle ="Recent Trends in Data Type Specifications",
publisher = "Springer",
year = 1996,
note = "LNCS, Volume 389"}

@book{manna-pnueli92,
author = "Zohar Manna and Amir Pnueli",
title = "The Temporal Logic of Reactive and Concurrent Systems",
publisher = "Springer",
address = "New York",
year = "1992"}

@book{manna-pnueli95,
author = "Zohar Manna and Amir Pnueli",
title = "Temporal Verification of Reactive Systems: Safety",
publisher = "Springer",
address = "New York",
year = "1995"}

@article{markov47,
author = "A. A. Markov",
title = "On the Impossibility of certain algorithms in the theory of
  associative systems",
journal = "Dokl. Akad. Nauk SSSR",
volume = 55,
number = 7,
pages = "587--590",
year = 1947,
note = "In Russian.  English translation in C. R. Acad. Sci. URSS, 55, 533-586"
}

@article{matijasevic67,
author = "J. V. Matijasevic",
title = "Simple Examples of Undecidable Associative Calculi",
journal = "Soviet Mathematics (Dokladi)",
volume = 8,
number = 2,
pages = "555--557",
year = 1967
}

@incollection{matsumiya-iida-futatsugi99,
title = "A Component-based Algebraic Specification of ODP Trading Function",
author = "Chiyo Matsumiya and Shusaku Iida and Kokichi Futatsugi",
editor = "Kokichi Futatsugi and Joseph Goguen and Jos{\' e} Meseguer",

booktitle = "OBJ/CafeOBJ/Maude at Formal Methods '99",
publisher = "Theta",
note = "Proceedings of a workshop held in
  Toulouse, France, 20th and 22nd September 1999",
year = 1999,
pages = "227--241"}

@inproceedings{matsumoto-futatsugi98,
author = "Michihiro Matsumoto and Kokichi Futatsugi",
title = "Test Set Coinduction -- Toward Automated Verification of
  Behavioral Properties",
booktitle = "Proceedings of the Second International
  Workshop on Rewriting Logic and Its Applications (WRLA'98)",
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
volume = 15,
publisher = "Elsevier Science",
year = "1998"}

@article{DBLP:journals/jar/Leroy09,
  author    = {Xavier Leroy},
  title     = {A Formally Verified Compiler Back-end},
  journal   = {J. Autom. Reasoning},
  volume    = {43},
  number    = {4},
  year      = {2009},
  pages     = {363-446}
}

@incollection{matsumoto-futatsugi99,
title = "Object Composition and Refinement by using Non-Observable
  Projection Operators",
author = "Michihiro Matsumoto and Kokichi Futatsigi",
editor = "Kokichi Futatsugi and Joseph Goguen and Jos{\' e} Meseguer",
booktitle = "OBJ/CafeOBJ/Maude at Formal Methods '99",
publisher = "Theta",
note = "Proceedings of a workshop held in
  Toulouse, France, 20th and 22nd September 1999",
year = 1999,
pages = "133--157"}

@techreport{mayoh85,
title = "Galleries and Institutions",
author = "Brian Mayoh",
year = 1985,
number = "DAIMI PB-191",
institution = "Aarhus University"}

@incollection{mccarthy-painter67,
author = "J. McCarthy and J. Painter",
title = "Correctness of a Compiler for Arithmetic Expressions",
booktitle = "Proc. Symposium in Applied Mathematics, Vol. 19, Mathematical Aspects of Computer Science",
publisher = "AMS",
address = "Providence, RI",
editor = "J. T. Schwartz",
pages = "33--41",
year = "1967",
url = "citeseer.nj.nec.com/250173.html"}

@incollection{mccarthy-painter67-fsh,
author = "J. McCarthy and J. Painter",
title = "Correctness of a Compiler for Arithmetic Expressions",
booktitle = "Proceedings of the Symposium in Applied Mathematics",
series = "Mathematical Aspects of Computer Science",
volume = 19,
pages = "33--41",
year = "1967"}

@incollection{meseguer-goguen85,
title = "Initiality, Induction and Computability",
author = "Jos\'e Meseguer and Joseph Goguen",
booktitle = "Algebraic Methods in Semantics",
editor = "Maurice Nivat and John Reynolds",
publisher = "Cambridge",
year = 1985,
pages = "459--541"}

@incollection{meseguer-goguen85-fsh,
title = "Initiality, Induction and Computability",
author = "J. Meseguer and J. Goguen",
booktitle = "Algebraic Methods in Semantics",
publisher = "Cambridge",
year = 1985,
pages = "459--541"}

@incollection{meseguer89,
author = "Jos\'e Meseguer",
title = "General Logics",
booktitle = "Proceedings, Logic Colloquium 1987",
publisher = "North-Holland",
editor = "H.-D. Ebbinghaus and others",
pages = "275--329",
year = 1989}

@incollection{mes-gen,
author = "Jos\'e Meseguer",
title = "General Logics",
booktitle = "Proceedings, Logic Colloquium 1987",
publisher = "North-Holland",
editor = "H.-D. Ebbinghaus and others",
pages = "275--329",
year = 1989}

@article{mes-rew,
author = "Jos\'{e} Meseguer",
title = "{Conditional Rewriting Logic as a Unified Model of Concurrency}",
journal = "Theor.\ Comput.\ Sci.",
pages = "73--155",
year = "1992"}

@book{agha-actors,
 author = {Agha, Gul},
 title = {Actors: a model of concurrent computation in distributed systems},
 year = {1986},
 publisher = {MIT Press},
 address = {Cambridge, MA, USA},
 }


@incollection{meseguer93,
author = "Jos\'e Meseguer",
title = "A Logical Theory of Concurrent Objects and its realization in the
  {Maude} Language",
booktitle = "Research Directions in Concurrent Object-Oriented Programming",
editor = "Gul Agha and Peter Wegner and Akinori Yonezawa",
year = "1993",
pages = "314--390",
publisher = "MIT Press"}

@inproceedings{mes-mem,
author = "Jos\'{e} Meseguer",
title = "Membership Algebra as a Logical Framework for Equational
Specification",
booktitle = "Proceedings, WADT'97",
series = "LNCS",
volume = 1376,
publisher = "Springer",
pages = "18--61",
year = 1998}

@inproceedings{meseguer98-sh,
author = "J. Meseguer",
title = "Membership Algebra as a Logical Framework for Equational
Specification",
booktitle = "Proceedings, WADT'97",
series = "LNCS",
volume = 1376,
pages = "18--61",
year = 1998}

@inproceedings{meseguer-rosu02b,
author = "Jos{\' e} Meseguer and Grigore Ro{\c s}u",
title = "Towards Behavioral Maude: Behavioral Membership Equational Logic",
booktitle = "Coalgebraic Methods in Computer Science, (CMCS'02)",
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
volume = "65",
year = 2002}

@inproceedings{meseguer-rosu02,
author = "Jos{\' e} Meseguer and Grigore Ro{\c s}u",
title = "A Total Approach to Partial Algebraic Specification",
booktitle = "International Conference on Automata, Languages and Programming
  (ICALP'02)",
series = "LNCS",
volume = "2380",
pages = "572--584",
year = 2002}

@unpublished{meseguer-rosu02-draft,
author = "Jos{\' e} Meseguer and Grigore Ro{\c s}u",
title = "A Total Approach to Partial Algebraic Specification",
note = "Submitted for publication.
  Extended version at \url{ase.arc.nasa.gov/grosu/tapase.html}",
year = 2002}

@unpublished{meseguer-rosu02-draft-fsh,
author = "J. Meseguer and G. Ro{\c s}u",
title = "A Total Approach to Partial Algebraic Specification",
note = "Extended version at \url{ase.arc.nasa.gov/grosu/tapase.html}",
year = 2002}

@incollection{mikami98,
title = "Semantics of equational specifications with module import and
  verification method of behavioral equations",
author = "Seik\^{o} Mikami",
booktitle = "Proceedings, CafeOBJ Symposium",
publisher = "Japan Advanced Institute for Science and Technology",
year = 1998,
note = "Numazu, Japan, April 1998"}

@incollection{mikami98-fsh,
title = "Semantics of equational specifications with module import and
  verification method of behavioral equations",
author = "S. Mikami",
booktitle = "Proceedings of CafeOBJ Symposium",
publisher = "Japan Advanced Institute for Science and Technology",
year = 1998}

@article{milner-tofte91,
author = "Robin Milner and Mads Tofte",
title = "Coinduction in relational semantics",
journal = "Theor.\ Comput.\ Sci.",
volume = "87",
number = "1",
pages = "209--220",
day = "16",
monthXXX = sep,
year = "1991"}

@book{mitchell65,
title = "Theory of categories",
author = "Mitchell, B.",
year = 1965,
publisher = "Academic Press, New York"}

@incollection{moore56,
author = "E. F. Moore",
title = "Gedanken--experiments on sequential machines",
booktitle = "Annals of Mathematics Studies (34), Automata Studies",
editor = "C. E. Shannon and J. McCarthy",
publisher = "Princeton University Press",
address = "Princeton, NJ",
pages = "129--153",
year = "1956"}

@incollection{mori-futatsugi99,
title = "Verifying Behavioural Specifications in CafeOBJ Environment",
author = "Akira Mori and Kokichi Futatsugi",
booktitle = "Proceedings of World Congress on Formal Methods (FM'99)",
series = "LNCSs",
volume = "1709",
publisher = "Springer",
pages = "1625--1643",
year = 1999}

@inproceedings{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},
  title     = {Mechanized Metatheory for the Masses: The {POPL}Mark Challenge},
  booktitle = {TPHOLs},
  year      = {2005},
  pages     = {50-65}
}


@misc{flyspec,
title = "The {F}lyspeck project",
note = "\url{https://code.google.com/p/flyspeck}",
year = ""}

@misc{agda,
title = "The {A}gda webpage",
note = "\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}",
year = ""}

@inproceedings{morris73,
author = "F. L. Morris",
title = "Advice on structuring compilers and proving them correct",
booktitle = "ACM Symposium on Principles of Programming Languages",
year = "1973",
pages = "144--152",
publisher = "Association for Computing Machinery"}

@inproceedings{morris73-fsh,
author = "F. L. Morris",
title = "Advice on structuring compilers and proving them correct",
booktitle = "Proceedings of POPL'73",
year = "1973",
pages = "144--152",
publisher = "ACM"}

@inproceedings{mossakowski96,
author = "Till Mossakowski",
title = "Equivalences among various logical frameworks of partial algebras",
booktitle = "Proceedings, Computer Science Logic (CSL'95)",
series = "LNCS",
volume = 1092,
publisher = "Springer",
pages = "403--433",
year = 1996}

@inproceedings{mossakowski96-sh,
author = "T. Mossakowski",
title = "Equivalences among various logical frameworks of partial algebras",
booktitle = "Computer Science Logic",
series = "LNCS",
volume = 1092,
pages = "403--433",
year = 1996}

@inproceedings{mossakowski96b,
author = "Till Mossakowski",
title = "Different Types of Arrow Between Logical Frameworks",
booktitle = "Proceedings, ICALP'96",
series = "LNCS",
volume = 1099,
publisher = "Springer",
pages = "158--169",
year = 1996}

@phdthesis{mossakowski-thesis,
title = "Representations, Hierarchies, and Graphs of Institutions",
author = "Till Mossakowski",
year = 1996,
school = "University of Bremen"}

@misc{mossakowski98,
title = "Version Control and Registration for {CASL} Libraries",
author = "Till Mossakowski",
note = "CoFi Note: M-5, 29 September 1998.
  {\tt http://www.brics.dk/Projects/CoFI/Notes/M-5}"}

@inproceedings{mossakowski00,
author = "Till Mossakowski",
title = "Specifications in an arbitrary institution with symbols",
booktitle = "Proceedings, WADT'99",
series = "LNCS",
volume = 1827,
publisher = "Springer",
pages = "252--270",
year = 2000}

@unpublished{hol-casl,
author = "Till Mossakowski",
title = "Introduction into {HOL-CASL}",
year = "2001",
note = {\url{http://www.tzi.de/cofi/}}}

@unpublished{hol-casl-sh,
author = "T. Mossakowski",
title = "Introduction into {HOL-CASL}",
year = "2001",
note = {\url{http://www.tzi.de/cofi/}}}

@article{mossakowski02,
title = "Relating {CASL} with Other Specification Languages:
  the Institution Level",
author = "Till Mossakowski",
year = "To appear",
note = "\url{http://www.tzi.de/~till/publications.html}",
journal = "Theor.\ Comput.\ Sci."}

@article{mossakowski02-sh,
title = "Relating {CASL} with Other Specification Languages:
  the Institution Level",
author = "T. Mossakowski",
year = "To appear",
note = "\url{http://www.tzi.de/\~{}till}",
journal = "Theor.\ Comput.\ Sci."}


@book{SanPiBook,
  title = {The $\pi$-calculus.  A theory of mobile processes},
  author = {Davide Sangiorgi and David Walker},
  publisher = "Cambridge",
  year = 2001,
  }

@article{mil-the,
title = "A Theory of Type Polymorphism in Programming",
author = "Robin Milner",
year = "1978",
volume = 17,
pages = "348--375",
journal = "J. Computer and System Sciences"}

@misc{mossakowski02b,
title = "Simplified Heterogeneous Specifications",
author = "Till Mossakowski",
note = "Submitted.  {\small\tt http://www.informatik.uni-bremen.de/~till}"}

@inproceedings{mossakowski-etal-02-fsh,
author = "T. Mossakowski and H. Reichel and M. Roggenbach and L. Schroder",
title = "Algebraic-coalgebraic specification in {CoCASL}",
booktitle = "Proceedings of WADT'02",
series = "LNCS",
volume = 2755,
publisher = "Springer",
pages = "376--392",
year = 2002}

@incollection{mosses89,
author = "Peter Mosses",
title = "Unified Algebras and Institutions",
year = 1989,
booktitle = "Proceedings, Fourth Annual Conference on Logic in Computer
  Science",
pages = "304--312",
publisher = "Institute of Electrical and Electronics Engineers"}

@InProceedings{necula97,
author = "George C. Necula",
title = "Proof-carrying code",
booktitle = "Proceedings of the 24th Symposium on Principles of Programming
  Languages (POPL'97)",
publisher = "ACM",
year = "1997",
pages = "106--119"}

@article{nemeti82,
title = "On notions of factorization systems and their applications to
   cone-injective subcategories",
author = "Istv{\' a}n N{\' e}meti",
journal = "Periodica Mathematica Hungarica",
year = 1982,
volume = 13,
number = 3,
pages ="229--335"}

@incollection{nemeti-sain81,
title = "Cone-implicational subcategories and some {B}irkhoff-type
theorems",
author = "Istv{\' a}n N{\' e}meti and Ildick{\' o} Sain",
booktitle = "Universal Algebra",
editor = "B. Csakany and E. Fried and E. T. Schmidt",
year = 1981,
publisher = "North-Holland",
pages = "535--578",
note = "Colloquia Mathematics Societas J{\' a}nos Bolyai, 29"}

@misc{nielsen-platet86,
title = "Polymorphism in an Institutional Framework",
author = "Mogens Nielsen and Udo Platet",
year = 1986,
note = "Technical University of Denmark"}

@inproceedings{nivela-orejas88,
author = "Pilar Nivela and Fernando Orejas",
title = "Initial behaviour semantics for algebraic
  specifications",
pages = "184--207",
ISBN = "3-540-50325-0",
editor = "D. Sannella; A. Tarlecki",
booktitle = "Proceedings of the 5th Workshop on Recent Trends in Data Type
  Specification",
monthXXX = sep,
series = "LNCS",
volume = "332",
publisher = "Springer",
address = "Berlin",
year = "1988"}

@inproceedings{olveczky-meseguer00,
author = "Peter Csaba Olveczky and Jos\'e Meseguer",
title = "{Real-Time} {Maude}: a tool for simulating and analyzing real-time
  and hybrid systems",
booktitle = {3rd International Workshop on Rewriting Logic and its Applications},
editor = "Kokichi Futatsugi",
year = "2000",
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
publisher = "Elsevier"}

@phdthesis{olveczky-thesis,
title = "Specification and Analysis of Real-Time and Hybrid Systems in
  Rewriting Logic",
author = "Peter Csaba Olveczky",
year = "2000",
school = "University of Bergen, Norway"}

@InProceedings{orejas-nivela-ehrig89,
author = "Fernando Orejas and Pilar Nivela and Hartmut Ehrig",
title = "Semantical constructions for categories of behavioural
  specifications.",
booktitle = "Proc. Workshop on Categorical Methods in Computer
  Science with Aspects from Topology",
publisher = "Springer LNCS 393",
pages = "220--241",
year = "1989"}

@article{padawitz-wirsing84,
author = "Peter Padawitz and Martin Wirsing",
title = "Completeness of many-sorted equational logic revisited",
journal = "Bulletin of the European Association for Theoretical
  Computer Science",
volume = "24",
pages = "88--94",
monthXXX = oct,
year = "1984"}

@inproceedings{padawitz96,
author = "Peter Padawitz",
title = "Swinging Data Types: Syntax, Semantics, and Theory",
booktitle = "Proceedings, WADT'95",
series = "LNCS",
volume = 1130,
publisher = "Springer",
pages = "409--435",
year = 1996}

@inproceedings{padawitz96-fsh,
author = "P. Padawitz",
title = "Swinging Data Types: Syntax, Semantics, and Theory",
booktitle = "Proceedings, WADT'95",
series = "LNCS",
volume = 1130,
publisher = "Springer",
pages = "409--435",
year = 1996}

@inproceedings{padawitz98,
author = "Peter Padawitz",
title = "Towards the One-Tiered Design of Data Types and Transition
Systems",
booktitle = "Proceedings, WADT'97",
series = "LNCS",
volume = 1376,
publisher = "Springer",
pages = "365--380",
year = 1998}

@inproceedings{padawitz98-fsh,
author = "P. Padawitz",
title = "Towards the One-Tiered Design of Data Types and Transition
Systems",
booktitle = "Proceedings of WADT'97",
series = "LNCS",
volume = 1376,
publisher = "Springer",
pages = "365--380",
year = 1998}

@misc{padawitz99,
title = "Integrating Functional-Logic and State-Oriented Specifications",
author = "Peter Padawitz",
year = "1999",
note = "WFLP '99.
  {\tt http://issan.informatik.uni-dortmund.de/~peter}"}

@article{padawitz00,
title = "Swinging Types = Functions + Relations + Transition Systems",
author = "Peter Padawitz",
journal = "Theor.\ Comput.\ Sci.",
volume = 243,
pages = "93--165",
year = "2000"}

@article{padawitz00-fsh,
title = "Swinging Types = Functions + Relations + Transition Systems",
author = "P. Padawitz",
journal = "Theor.\ Comput.\ Sci.",
volume = 243,
pages = "93--165",
year = "2000"}

@book{papadimitriou94,
author = "Christos H. Papadimitriou",
title = "Computational Complexity",
publisher = "Addison-Wesley",
address = "New York",
year = "1994"}

@inproceedings{park-stern-dill00,
author = "David Y. W. Park and Ulrich Stern and David L. Dill",
title = "{Java Model Checking}",
booktitle = "Proceedings of the First International Workshop on
  Automated Program Analysis, Testing and Verification, Limerick, Ireland",
year = "2000",
monthXXX = jun}

@article{parnas72,
author = "David Parnas",
title = "Information Distribution Aspects of Design Methodology",
journal = "Information Processing '72",
volume = 71,
pages = "339--344",
year = 1972,
publisher = "IFIP",
note = "Proceedings of 1972 IFIP Congress"}

@article{parnas72-fsh,
author = "D. Parnas",
title = "Information Distribution Aspects of Design Methodology",
journal = "Information Processing",
volume = 71,
pages = "339--344",
year = 1972,
publisher = "IFIP"}

@inproceedings{pattinson00,
author = "Dirk Pattinson",
title = "Modal Logic for Rewriting Theories",
booktitle = "Proceedings of the 3rd International Workshop on Rewriting Logic
  and its Applications",
editor = "Kokichi Futatsugi",
year = 2000,
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
volume = 36,
pages = "173--191",
publisher = "Elsevier"}

@inproceedings{pawlowski96,
title = "Context Institutions",
author = "Wieslaw Pawlowski",
booktitle = {Recent Trends in Data Type Specification},
editor = {Magne Haveraaen and Olaf Owe and Ole-Johan Dahl},
publisher = "Springer",
series = "LNCS",
volume = 1130,
pages = {436--457},
year = 1996,
note = {Proceedings of 11th Workshop on Specification of Abstract Data
  Types. Oslo, Norway, September 1995}}

@article{pigozzi74,
title = "The Join of Equational Thories",
author = "Don Pigozzi",
journal = "Colloquium Mathematicum",
year = 1974,
volume = 30,
pages = "15--25"}

@article{post47,
author = "Emil L. Post",
title = "Recursive Unsolvability of a problem of Thue",
journal = "Journal of symbolic Logic",
volume = 13,
pages = "1--11",
year = "1947"
}

@article{takahashi-CompleteDevelopment,
  author    = {Masako Takahashi},
  title     = {Parallel Reductions in lambda-Calculus},
  journal   = {Inf. Comput.},
  volume    = {118},
  number    = {1},
  year      = {1995},
  pages     = {120--127},
}


@article{badouel-OnGuardedRecursion,
  author    = {Eric Badouel and Philippe Darondeau},
  title     = {On guarded recursion},
  journal   = {Theor. Comput. Sci.},
  volume    = {82},
  year      = {1991},
  pages     = {403--408},
}


@article{plotkin-SOS,
  author    = {Gordon D. Plotkin},
  title     = {A structural approach to operational semantics},
  journal   = {J. Log. Algebr. Program.},
  volume    = {60-61},
  year      = {2004},
  pages     = {17--139}
}


@inproceedings{DBLP:conf/popl/HurNDV13,
  author    = {Chung-Kil Hur and
               Georg Neis and
               Derek Dreyer and
               Viktor Vafeiadis},
  title     = {The power of parameterization in coinductive proof},
  booktitle = {POPL},
  year      = {2013},
  pages     = {193-206}
}



@article{plotkin-CBNandCBVandLambda,
  author    = {Gordon D. Plotkin},
  title     = {Call-by-Name, Call-by-Value and the lambda-Calculus},
  journal   = {Theor. Comput. Sci.},
  volume    = {1},
  number    = {2},
  year      = {1975},
  pages     = {125--159},
}

@article{DBLP:journals/mscs/Bartels03,
  author    = {Falk Bartels},
  title     = {Generalised Coinduction},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {13},
  number    = {2},
  year      = {2003},
  pages     = {321-348}
}


@inproceedings{turi-plotkin97,
title = "Towards a Mathematical Operational Semantics",
author = "Daniele Turi and Gordon Plotkin",
pages = "280--291",
booktitle = "LICS",
year = "1997"}

@incollection{poigne89,
title = "Foundations are Rich Institutions, but Institutions are Poor
  Foundations",
author = "Axel Poign\'e",
booktitle = "Categorical Methods in Computer Science",
editor = "Hartmut Ehrig and Horst Herrlich and Hans-J{\"o}rg Kerowski and
  Gerhard Preuss",
publisher = "Springer",
pages = "82--101",
note = "LNCS, Volume 393",
year = 1989}

@article{poigne90p,
title = "Parameterization for Order-Sorted Algebraic Specification",
author = "Axel Poign\'e",
journal = "Journal of Computer and System Sciences",
volume = 40,  number = 3,
year = 1990,
pages = "229--268"}

@misc{PolySpace,
Author = {PolySpace},
Note = {URL: {\footnotesize\tt http://www.polyspace.com}}}

@inproceedings{pnueli77,
author = "Amir Pnueli",
title = "{The Temporal Logic of Programs}",
booktitle = "Proceedings of the 18th IEEE Symposium on Foundations of
  Computer Science",
year = 1977,
pages = "46--77"}

@incollection{reichel81,
title = "Behavioural Equivalence -- A Unifying Concept for Initial and Final
  Specifications",
author = "Horst Reichel",
editor = "M. Arata and L. Varga",
year = 1981,
booktitle = "Proceedings, Third Hungarian Computer Science Conference",
publisher = "Akademiai Kiado",
note = "Budapest"}

@incollection{reichel81-fsh,
title = "Behavioural Equivalence -- A Unifying Concept for Initial and Final
  Specifications",
author = "H. Reichel",
year = 1981,
booktitle = "Proceedings of the 3rd Hungarian Computer Science Conference",
publisher = "Akademiai Kiado"}

@book{reichel84,
author = "Horst Reichel",
title = "Structural Induction on Partial Algebras",
year = 1984,
publisher = "Akademie-Verlag Berlin"}

@incollection{reichel85,
title = "Behavioural Validity of Conditional Equations in Abstract Data
  Types",
author = "Horst Reichel",
year = 1985,
booktitle = "Contributions to General Algebra 3",
publisher = "Teubner",
note = "Proceedings of the Vienna Conference, June 21-24, 1984"}

@incollection{reichel85-fsh,
title = "Behavioural Validity of Conditional Equations in Abstract Data
  Types",
author = "H. Reichel",
year = 1985,
booktitle = "Contributions to General Algebra 3",
publisher = "Teubner"}

@book{reichel87,
author = "Horst Reichel",
title = "Initial Computability, Algebraic Specifications, and Partial
  Algebras",
publisher = "Oxford University Press",
year = "1987"}

@book{reichel87-sh,
author = "H. Reichel",
title = "Initial Computability, Algebraic Specifications, and Partial
  Algebras",
publisher = "Oxford University Press",
year = "1987"}

@article{reichel95,
title = "An approach to object semantics based on terminal co-algebras",
author = "Horst Reichel",
journal = "Mathematical Structures in Computer Science",
year = 1995,
volume = 5,
pages = "129--152"}

@techreport{reichel98,
author = "Horst Reichel",
title = "Nested Sketches",
year = 1998,
institution = "University of Edinburgh",
number = "ECS-LFCS-98-401"}

@misc{reichel02,
title = "Formal Specification of Data and Process Types",
author = "Horst Reichel",
note = "Course notes, summer term 2002, ITI, Dresden, Germany"}

@article{rice53,
author = "Gordon H. Rice",
title = "Classes of Recursively Enumerable Sets and their Decision
problems",
year = "1953",
journal = "Transactions of the American Mathematical Society",
volume = "74",
pages = "358--366"}

@techreport{rod-first,
author = "Pieter Hendrik Rodenburg and Rob van Glabbeek",
title = "An Interpolation Theorem in Equational Logic",
year = 1988,
institution = "CWI",
number = "CS-R8838"}

@article{rod-sim,
title = "A Simple Algebraic Proof of the Equational Interpolation Theorem",
author = "Pieter Hendrik Rodenburg",
year = 1991,
journal = "Algebra Universalis",
volume = 28, pages = "48--51"}

@book{rogers87,
author = "Hartley {Rogers Jr.}",
title = "Theory of Recursive Functions and Effective Computability",
year = "1987",
publisher = "MIT press",
address = "Cambridge, MA"}

@article{rosen73,
title = "Tree-Manipulating Systems and {C}hurch-{R}osser Theorems",
author = "Barry Rosen",
journal = "Journal of the Association for Computing Machinery",
year = 1973,
monthXXX = jan,
pages = "160--187"}

@article{rosen73-fsh,
title = "Tree-Manipulating Systems and {C}hurch-{R}osser Theorems",
author = "B. Rosen",
journal = "Journal of the Association for Computing Machinery",
year = 1973,
monthXXX = jan,
pages = "160--187"}

@article{rosu94,
title = "The Institution of Order-Sorted Equational Logic",
author = "Grigore Ro\c{s}u",
journal = "Bulletin of EATCS",
year = 1994,
volume = 53,
pages ="250--255"}

@article{rosu01,
author = "Grigore Ro\c{s}u",
title = "Axiomatizability in Inclusive Equational Logics",
journal = "Mathematical Structures in Computer Science",
note= "{\tt http://ase.arc.nasa.gov/grosu/iel.ps}",
year = "to appear"}

@misc{rosu96,
title = "Axiomatizability in Inclusive Equational Logic",
author = "Grigore Ro\c{s}u",
note = "Submitted for publication",
year = 1996}

@inproceedings{rosu98,
title = "A \textUp{B}irkhoff-like Axiomatizability Result for Hidden Algebra
  and Coalgebra",
author = "Grigore Ro\c{s}u",
booktitle = {Proceedings of the First Workshop on Coalgebraic Methods
  in Computer Science (CMCS'98), Lisbon, Portugal, March 1998},
publisher = "Elsevier Science",
editor = "Bart Jacobs and Larry Moss and Horst Reichel and Jan Rutten",
pages = "179--196",
volume = 11,
series = "Electr.\ Notes Theor.\ Comput.\ Sci.",
year = 1998}

@inproceedings{rosu98-fsh,
title = "A \textUp{B}irkhoff-like Axiomatizability Result for Hidden Algebra
  and Coalgebra",
author = "G. Ro\c{s}u",
booktitle = "Proceedings of CMCS'98",
publisher = "Elsevier",
pages = "179--196",
volume = 11,
series = "ENTCS",
year = 1998}

@incollection{rosu-goguen98,
author = "Grigore Ro\c{s}u and Joseph Goguen",
title = "Hidden Congruent Deduction",
year = 2000,
editor = "Ricardo Caferra and Gernot Salzer",
publisher = "Springer",
booktitle = "Automated Deduction in Classical and Non-Classical Logics",
note = "Lecture Notes in Artificial Intelligence, Volume 1761; papers from
  First Order Theorem Proving '98 (FTP'98), Vienna, November 1998",
pages = "252--267"}

@incollection{rosu-goguen00,
author = "Grigore Ro\c{s}u and Joseph Goguen",
title = "Hidden Congruent Deduction",
year = 2000,
editor = "Ricardo Caferra and Gernot Salzer",
publisher = "Springer",
booktitle = "Automated Deduction in Classical and Non-Classical Logics",
series = "Lecture Notes in Artificial Intelligence",
volume = "1761",
note = "Papers from First Order Theorem Proving '98 (FTP'98)",
pages = "252--267"}

@incollection{rosu-goguen00-sh,
author = "Grigore Ro\c{s}u and Joseph Goguen",
title = "Hidden Congruent Deduction",
year = 2000,
editor = "Ricardo Caferra and Gernot Salzer",
publisher = "Springer",
booktitle = "Automated Deduction in Classical and Non-Classical Logics",
series = "Lecture Notes in Artificial Intelligence",
volume = "1761",
pages = "252--267"}

@incollection{rosu-goguen00-fsh,
author = "G. Ro\c{s}u and J. Goguen",
title = "Hidden Congruent Deduction",
year = 2000,
publisher = "Springer",
booktitle = "Automated Deduction in Classical and Non-Classical Logics",
series = "LNAI",
volume = "1761"}

@incollection{rosu-goguen01,
author = "Grigore Ro\c{s}u and Joseph Goguen",
title = "Circular Coinduction",
year = 2001,
booktitle = "International Joint Conference on Automated Reasoning
(IJCAR'01)",
note = "Short paper.  An extended version appeared as UCSD
  Technical Report CSE2000--0647"}

@incollection{rosu-goguen01-fsh,
author = "G. Ro\c{s}u and J. Goguen",
title = "Circular Coinduction",
year = 2001,
booktitle = "International Joint Conference on Automated Reasoning
(IJCAR'01)",
note = "Short paper.  An extended version appeared as UCSD
  Technical Report CSE2000--0647"}

@techreport{rosu-goguen00b,
author = "Grigore Ro\c{s}u and Joseph Goguen",
title = "Circular Coinduction",
year = "written October 1999",
institution = "University of California at San Diego",
number = "CSE2000--0647"}

@techreport{rosu-segerlind99,
author = "Grigore Ro\c{s}u and Nathan Segerlind",
title = "Proofs of Safety for Untrusted Code",
year = "1999",
institution = "University of California at San Diego",
number = "CSE2000--0633"}

@article{wis2,
title = "Weak Inclusion Systems; part 2",
author = "Virgil Emil C\u{a}z\u{a}nescu and Grigore Ro\c{s}u",
year = 2000,
journal = "Journal of Universal Computer Science",
volume = 6,
number = 1,
pages = "5--21"}

@article{ros-equ,
title = "On Equational {C}raig Interpolation",
author = "Grigore Ro\c{s}u and Joseph Goguen",
year = 2000,
journal = "Journal of Universal Computer Science",
volume = 6,
number = 1,
pages = "194--200"}

@incollection{rosu-whittle02,
title = "Towards Certifying Domain-Specific Properties of Synthesized Code",
author = "Grigore Ro\c{s}u and Jonathan Whittle",
booktitle = "Proceedings, International Conference on
  Automated Software Engineering (ASE'02)",
publisher = "Institute of Electrical and Electronics Engineers",
year = 2002,
note = "Edinburgh, Scotland"}

@article{inst,
title = "Kan Extensions of Institutions",
author = "Grigore Ro\c{s}u",
year = 1999,
journal = "Journal of Universal Computer Science",
volume = 5,
number = 8,
pages = "482--493"}

@techreport{mod,
author = "Grigore Ro\c{s}u",
title = "Abstract Semantics for Module Composition",
year = "May 2000",
institution = "University of California at San Diego",
number = "CSE2000--0653"}

@techreport{mod-fsh,
author = "G. Ro\c{s}u",
title = "Abstract Semantics for Module Composition",
year = "May 2000",
institution = "University of California at San Diego",
number = "CSE2000--0653"}

@incollection{brew,
title = "Behavioral Coinductive Rewriting",
author = "Grigore Ro\c{s}u",
editor = "Kokichi Futatsugi and Joseph Goguen and Jos{\' e} Meseguer",
booktitle = "OBJ/CafeOBJ/Maude at Formal Methods '99",
publisher = "Theta",
note = "Proceedings of a workshop held in
  Toulouse, France, 20th and 22nd September 1999",
year = 1999,
pages = "179--196"}

@article{rosu01c,
author = "Grigore Ro\c{s}u",
title = "Equational Axiomatizability for Coalgebra",
journal = "Theor.\ Comput.\ Sci.",
year = "2001",
volume = "260",
number = "1-2",
pages = "229--247"}

@article{rosu01c-fsh,
author = "G. Ro\c{s}u",
title = "Equational Axiomatizability for Coalgebra",
journal = "Theor.\ Comput.\ Sci.",
year = "2001",
volume = "260",
number = "1-2",
pages = "229--247"}

@phdthesis{rosu-thesis,
title = "Hidden Logic",
author = "Grigore Ro\c{s}u",
year = 2000,
school = "University of California at San Diego",
note = "{\small\tt http://ase.arc.nasa.gov/grosu/phd-thesis.ps}"}

@phdthesis{rosu-thesis-fsh,
title = "Hidden Logic",
author = "G. Ro\c{s}u",
year = 2000,
school = "University of California at San Diego"}

@misc{rosu-master,
title = "Axiomatizare \^{\i}n Logica Inclusiv\u{a}",
author = "Grigore Ro\c{s}u",
year = 1996,
school = "Universitatea Bucure\c{s}ti"}

@incollection{rosu01b,
author = "Grigore Ro\c{s}u",
title = "Complete Categorical Equational Deduction",
year = "2001",
editor = "Laurent Fribourg",
publisher = "Springer",
booktitle = "Proceedings of Computer Science Logic (CSL'01)",
series = "LNCS",
volume = "2142",
location = "Paris, France",
pages = "528--538"}

@techreport{rosu-havelund01,
author = "Grigore Ro\c{s}u and Klaus Havelund",
title = "{Synthesizing Dynamic Programming Algorithms from Linear
  Temporal Logic Formulae}",
year = "May 2001",
institution = "NASA--RIACS",
number = "TR 01-08"}

@article{pitts-AlphaStructural,
  author    = {Andrew M. Pitts},
  title     = {Alpha-structural recursion and induction},
  journal   = {J. ACM},
  volume    = {53},
  number    = {3},
  year      = {2006},
}

@inproceedings{rosu02,
 author = {Grigore Ro\c{s}u},
 title = {On implementing behavioral rewriting},
 booktitle = {Proceedings of the 2002 ACM SIGPLAN workshop on Rule-based programming},
 year = {2002},
 isbn = {1-58113-606-4},
 pages = {43--52},
 location = {Pittsburgh, Pennsylvania},
 publisher = {ACM},
 }

@inproceedings{rosu02-fsh,
 author = {G. Ro\c{s}u},
 title = {On implementing behavioral rewriting},
 booktitle = {Proceedings of the ACM SIGPLAN RULE'02},
 year = {2002},
 pages = {43--52},
 publisher = {ACM},
 }

@incollection{rosu-et-al03,
title = "Certifying Optimality of State Estimation Programs",
author = "Grigore Ro\c{s}u and Ram prasad Venkatesan and Jon Whittle and Laurentiu Leustean",
booktitle = "Computer Aided Verification (CAV'03)",
publisher = "Springer",
note = "to appear in LNCS",
year = 2003}

@inproceedings{DBLP:conf/fossacs/Rosu07,
  author    = {Grigore Ro\c{s}u},
  title     = {An Effective Algorithm for the Membership Problem for Extended
               Regular Expressions},
  booktitle = {FoSSaCS},
  year      = {2007},
  pages     = {332--345}
}

@inproceedings{rosu-viswanathan03,
author = "Grigore Ro\c{s}u and Mahesh Viswanathan",
title = "Testing Extended Regular Language Membership Incrementally by Rewriting",
booktitle = "Rewriting Techniques and Applications (RTA'03)",
year = "2003",
series = "LNCS, to appear",
publisher = "Springer"}

@article{rothe-etal-01,
author = "J. Rothe and B. Jacobs and H. Tews",
title = "The coalgebraic class specification language {CCSL}",
journal = "Journal of Universal Computer Science",
volume = 7,
pages = "175--193",
year = 2001}

@book{rudeanu63,
author = "Sergiu Rudeanu",
title = "Axiomele laticilor \c{s}i ale algebrelor
  booleene\footnote{Lattice and Boolean Algebra Axioms.}",
year = "1963",
publisher = "Romanian Academy Press",}

@incollection{rutten-turi94,
title = "Initial Algebra and Final Coalgebra Semantics for Concurrency",
author = "Jan Rutten and Daniele Turi",
booktitle = "Proc.\ {REX} Symposium `A Decade of Concurrency'",
editor = "Jaco de Bakker and Jan Willem de Roever and Gregorz Rozenberg",
publisher = "Springer",
note = "LNCS, Volume 803",
pages = "530--582",
year = 1994}

@article{rutten00,
author = "J. J. M. M. Rutten",
title = "Universal coalgebra: A theory of systems",
journal = "Theor.\ Comput.\ Sci.",
volume = 249,
pages = "3--80",
year = 2000}

@techreport{rutten96,
author = "J. J. M. M. Rutten",
title = "Universal coalgebra: a theory of systems",
year = 1996,
institution = "CWI",
number = "CS-R9652"}

@inproceedings{rutten99,
author = "Jan Rutten",
title = "Automata, Power series, and coinduction: taking input derivatives
  seriously",
booktitle = "Automata, Languages and Programming 26th ICALP'99",
year = "1999",
volume = "1644",
editor = "J. Wiedermann and P. van Emde Boas and M. Nielsen",
series = "LNCS",
pages = "645--654"}

@phdthesis{sampaio-thesis-fsh,
author = "A. Sampaio",
title =	"An Algebraic Approach to Compiler Design",
school = "Oxford University",
year = "1993"}

@phdthesis{tiu-thesis,
author = "Alwen Tiu",
title =	"A Logical Framework for Reasoning about Logical Specifications",
school = "Penn State University",

year = "2004"}

@phdthesis{schurman-thesis,
author = "C. Schurmann",
title =	"Automating the meta-theory of deductive systems",
school = "Carnegie Mellon University",
year = "2000"}

@INPROCEEDINGS{schurmanPfenning-automatedtheorem,
    author = {Carsten Schurmann and Frank Pfenning},
    title = {Automated theorem proving in a simple meta-logic for {L}{F}},
    booktitle = {CADE},
    year = {1998},
    pages = {286--300}
}


@incollection{sannella-tarlecki86,
author = "Donald Sannella and Andrzej Tarlecki",
title = "Extended {ML}: an institution independent framework for formal
  program development",
year = 1986,
booktitle = "Proceedings, Summer Workshop on Category Theory and Computer
  Programming",
location = "University of Surrey, Guildford, U.K.",
publisher = "Springer",
note = "LNCS, Volume 240",
pages = "364--389",
editor = "David Pitt and Samson Abramsky and Axel Poign\'e and David
  Rydeheard"}

@article{sannella-tarlecki87,
title = "On Observational Equivalence and Algebraic Specification",
author = "Donald Sannella and Andrzej Tarlecki",
year = 1987,
journal = "Journal of Computer and System Science",
volume = 34,
pages = "150--178",
note = "Also in Proceedings of the International Joint Conference on
  Theory and Practice of Software Development (TAPSOFT), Berlin.
  Volume 1: Colloquium on Trees in Algebra and Programming (CAAP 1985),
  {\em LNCS 185}, pages 308--322."}

@article{sannella-tarlecki87-sh,
title = "On Observational Equivalence and Algebraic Specification",
author = "Donald Sannella and Andrzej Tarlecki",
year = 1987,
journal = "Journal of Computer and System Science",
volume = 34,
pages = "150--178"}

@article{sannella-tarlecki87-fsh,
title = "On Observational Equivalence and Algebraic Specification",
author = "D. Sannella and A. Tarlecki",
year = 1987,
journal = "Journal of Computer and System Science",
volume = 34,
pages = "150--178"}

@article{san-spe,
author = "Donald Sannella and Andrzej Tarlecki",
title = "Specifications in an Arbitrary Institution",
year = 1988,
journal = "Information and Control",
volume = 76,
pages = "165--210"}

@article{sannella-tarlecki88a,
author = "Donald T. Sannella and Andrzej Tarlecki",
title = "Toward formal development of programs from algebraic
  specifications: implementations revisited.",
journal = "Acta Informatica",
volume = "25",
number = "3",
pages = "233--281",
monthXXX = apr,
year = "1988"}

@inproceedings{sannella-wirsing83,
title = "A Kernel Language for Algebraic Sepcification and Implementation",
author = "Donald Sannella and Martin Wirsing",
booktitle = {Colloquium on Foundations of Computation Theory},
editor = {Magne Haveraaen and Olaf Owe and Ole-Johan Dahl},
publisher = "Springer",
series = "LNCS",
volume = 158,
pages = {413--427},
year = 1983}

@inproceedings{sal-sof,
author = "Antonio Salibra and Giuseppe Scollo",
title = "A soft stairway to institutions",
editor = "Michel Bidoit and Christine Choppy",
booktitle = "Recent Trends in Data Type Specification",
series = "LNCS",
volume = "655",
publisher = "Springer",
year = "1992",
pages = "310--329"}

@article{sal-int,
title = "Interpolation and
compactness in categories of pre-institutions",
author = "Antonio Salibra and Giuseppe Scollo",
journal = "Math. Struct. in
Comp. Science",
year = 1996,
volume = 6,
pages = "261--286"}


@book{schubert72,
title = "Categories",
author = "Horst Schubert",
year = 1972,
publisher = "Springer"}

@manual{pvs-tutorial,
title = {PVS Tutorial},
author = {N. Shankar and S. Owre and J. M. Rushby},
monthXXX = feb,
year = 1993,
organization = {Computer Science Laboratory, SRI International},
address = {Menlo Park, CA},
note = {Also appears in Tutorial Notes, {\em Formal Methods Europe
  '93: Industrial-Strength Formal Methods}, pages 357--406,
   Odense, Denmark, April 1993}}

@inproceedings{silva94-fsh,
author = "F. da Silva",
title = "On Observational Equivalence and Compiler Correctness",
booktitle = "Proceedings ICCI'94",
pages = "17--34",
year = "1994",
series = "International Conf. on Computing and Information"}

@Book{sipser96,
author = "Michael Sipser",
title = "Introduction to the Theory of Computation",
publisher = "PWS",
year = "1996",
address = "Boston, MA",
}

@incollection{smolka-creas87-sh,
title = "Order-Sorted Equational Computation",
author = "Gert Smolka and Werner Nutt and Joseph Goguen and Jos\'e
Meseguer",
booktitle = "Resolution of Equations in Algebraic Structures, Volume 2:
  Rewriting Techniques",
editor = "Maurice Nivat and Hassan A{\"\i}t-Kaci",
publisher = "Academic",
pages = "299--367",
year = 1989}

@techreport{smolka86,
title = "Order-Sorted {H}orn Logic: Semantics and Deduction",
author = "Gert Smolka",
year = 1986,
number = "SEKI Report SR-86-17",
institution = "Fachbereich Informatik, Universit{\"a}t Kaiserslautern"}

@misc{stefaneas93,
author = "Petros Stefaneas",
title = "Chartering some Institutions",
note = "MSc Thesis, Programming Research Group, Oxford University",
year = 1993}

@inproceedings{stoller00,
author = "Scott D. Stoller",
title = "{Model-Checking Multi-threaded Distributed Java Programs}",
booktitle = "SPIN Model Checking and Software Verification",
series = "LNCS",
volume = 1885,
year = 2000,
editor = "Klaus Havelund and John Penix and Willem Visser",
pages = "224--244",
publisher = "Springer"}

@book{stoy77,
author = "Joseph Stoy",
title = "Denotational Semantics of Programming Languages: The Scott-Strachey
  Approach to Programming Language Theory",
year = 1977,
publisher = "MIT"}

@book{stoy77-fsh,
author = "J. Stoy",
title = "Denotational Semantics of Programming Languages: The Scott-Strachey
  Approach to Programming Language Theory",
year = 1977,
publisher = "MIT"}

@incollection{strachey66,
title = "Towards a Formal Semantics",
author = "Christopher Strachey",
booktitle = "Formal Language Description Languages",
editor = "Steel",
year = 1966,
pages = "198--220",
publisher = "North-Holland"}

@incollection{strachey66-fsh,
title = "Towards a Formal Semantics",
author = "C. Strachey",
booktitle = "Formal Language Description Languages",
editor = "Steel",
year = 1966,
pages = "198--220",
publisher = "North-Holland"}

@incollection{tarlecki84,
title = "Free Constructions in Algebraic Institutions",
author = "Andrzej Tarlecki",
booktitle = "Proceedings, International Symposium on Mathematical
Foundations
  of Computer Science",
editor = "M. P. Chytil and V. Koubek",
location = "Prague",
year = 1984,
pages = "526--534",
publisher = "Springer"}

@incollection{tar-bit,
author = "Andrzej Tarlecki",
title = "Bits and Pieces of the Theory of Institutions",
year = 1986,
booktitle = "Proceedings, Summer Workshop on Category Theory and Computer
  Programming, LNCS",
location = "University of Surrey, Guildford, U.K.",
publisher = "Springer",
volume="240",
pages = "334--360",
editor = "David Pitt and Samson Abramsky and Axel Poign\'e and David
  Rydeheard"}

@article{tar-exi,
title = "On the Existence of Free Models in Abstract Algebraic
Institutions",
author = "Andrzej Tarlecki",
journal = "Theor.\ Comput.\ Sci.",
year = 1986,
volume = 37,
pages = "269--304"}

@article{tar-qua,
title = "Quasi-Varieties in Abstract Algebraic Institutions",
author = "Andrzej Tarlecki",
journal = "Journal of Computer and System Sciences",
year = 1986,
volume = 33,
number = 3,
pages ="333--360"}

@misc{abella,
title = "The {A}bella {T}heorem Prover",
note = "\url{http://abella.cs.umn.edu}",
year = "2013"}

@misc{mck,
title = "Model-Checking Knowledge ({MCK})",
note = "\url{http://cgi.cse.unsw.edu.au/~mck/pmck}",
year = "2014"}

%%% TODO: Complete
@inproceedings{AbelA99,
  author    = {Andreas Abel and
               Thorsten Altenkirch},
  title     = {A Predicative Strong Normalisation Proof for a lambda-Calculus
               with Interleaving Inductive Types},
  booktitle = {TYPES~'99},
  pages     = {21--40},
  editor    = {Thierry Coquand and
               Peter Dybjer and
               Bengt Nordstr{\"o}m and
               Jan M. Smith},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {1956},
  year      = {2000}
}

@article{DBLP:journals/jar/McCune97,
  author    = {William McCune},
  title     = {Solution of the Robbins Problem},
  journal   = {J. Autom. Reasoning},
  volume    = {19},
  number    = {3},
  year      = {1997},
  pages     = {263-276}
}

@misc{twelf,
title = "The {T}welf {P}roject",
note = "\url{http://twelf.plparty.org}",
year = ""
}

@inproceedings{DBLP:conf/ascm/Gonthier07,
  author    = {Georges Gonthier},
  title     = {The Four Colour Theorem: Engineering of a Formal Proof},
  booktitle = {ASCM},
  year      = {2007},
  pages     = {333}
}

@misc{breakthrough,
title = "{MIT} Technology Review",
note = "\url{http://www2.technologyreview.com/article/423692/crash-proof-code}",
year = "2011"
}

@article{DBLP:journals/tocl/AvigadDGR07,
  author    = {Jeremy Avigad and
               Kevin Donnelly and
               David Gray and
               Paul Raff},
  title     = {A formally verified proof of the prime number theorem},
  journal   = {ACM Trans. Comput. Log.},
  volume    = {9},
  number    = {1},
  year      = {2007},
}

@misc{mizar,
title = "The {M}izar Home Page",
note = "\url{http://mizar.uwb.edu.pl}",
year = ""}

@misc{tarlecki87,
author = "Andrzej Tarlecki",
title = "Institution Representation",
note = "Unpublished note, Dept. of Computer Science,
  Univ. of Edinburgh",
year = "1987"}

@article{tarlecki-burstall-goguen91,
title = "Some Fundamental Algebraic Tools for the Semantics of Computation,
  Part 3: Indexed Categories",
author = "Andrzej Tarlecki and Rod Burstall and Joseph Goguen",
journal = "Theor.\ Comput.\ Sci.",
year = 1991,
volume = 91,
pages = "239--264"}

@article{jordan-curve-mizar,
title = "Jordan curve theorem",
author = "A. Kornilowicz",
journal = "Formalized Mathematics",
year = 2005,
volume = 13,
pages = "481--491"}

@inproceedings{tarlecki96,
title = "Moving between logical systems",
author = "Andrzej Tarlecki",
booktitle = {Recent Trends in Data Type Specification},
editor = {Magne Haveraaen and Olaf Owe and Ole-Johan Dahl},
publisher = "Springer",
series = "LNCS",
volume = 1130,
pages = {478--502},
year = 1996,
note = {Proceedings of 11th Workshop on Specification of Abstract Data
  Types. Oslo, Norway, September 1995}}

@inproceedings{tarlecki96-sh,
title = "Moving between logical systems",
author = "Andrzej Tarlecki",
booktitle = {Recent Trends in Data Type Specification},
editor = {Magne Haveraaen and Olaf Owe and Ole-Johan Dahl},
publisher = "Springer",
series = "LNCS",
volume = 1130,
pages = {478--502},
year = 1996}

@techreport{tarlecki96a,
author = "Andrzej Tarlecki",
title = "Structural Properties of Some Categories of Institutions",
institution = "Institute of Informatics, Warsaw University",
year = 1996}

@article{tarski44,
title = "The Semantic Conception of Truth",
author = "Alfred Tarski",
year = 1944,
journal = "Philos. Phenomenological Research",
volume = 4, pages = "13--47"}

@inproceedings{tews00-fsh,
title = "Coalgebras for Binary Methods",
author = "H. Tews",
booktitle = "Proceedings of CMCS'00",
publisher = "Elsevier",
volume = 33,
series = "ENTCS",
year = 2000}

@article{tews01-fsh,
title = "Coalgebras for Binary Methods: Properties of
  Bisimulations and Invariants",
author = "H. Tews",
year = 2001,
journal = "Theoretical Informatics and Applications",
volume = 35,
number = 1,
pages = "83--111"}

@inproceedings{tews02-fsh,
title = "Greatest Bisimulations for Binary Methods",
author = "H. Tews",
booktitle = "Proceedings of CMCS'02",
publisher = "Elsevier",
volume = "65(1)",
series = "ENTCS",
year = 2002}

@article{thatcher-wagner-wright79,
author = "J. W. Thatcher and E. G. Wagner and J. B. Wright",
title = "More on Advice on structuring Compilers and proving them correct",
journal = "LNCS",
year = "1979",
volume = "71",
pages = "596--615",
publisher = "Springer",
address = "Berlin Heidelberg"}

@inproceedings{thatcher-wagner-wright79-fsh,
author = "J. W. Thatcher and E. G. Wagner and J. B. Wright",
title = "More on Advice on structuring Compilers and proving them correct",
series = "LNCS",
year = "1979",
volume = "71",
publisher = "Springer"}

@inproceedings{tracz93,
author = "William Tracz",
title = "{\sc lileanna}: a Parameterized Programming Language",
booktitle = "Proceedings, Second International Workshop on Software Reuse",
monthXXX = "March",
year = 1993,
note = "Lucca, Italy",
pages = "66--78"}

@phdthesis{veglioni98,
title = "Integrating Static and Dynamic Aspects in the Specification
  of Open, Object-based and Distributed Systems",
author = "Simone Veglioni",
school = "Oxford University Computing Laboratory",
year = 1998}

@inproceedings{visser-et-al00,
author = "Willem Visser and Klaus Havelund and Guillaume Brat and
  SeungJoon Park",
title = "{Model Checking Programs}",
booktitle = "Proceedings of ASE'2000: The 15th IEEE International Conference
  on Automated Software Engineering",
publisher   = "IEEE CS Press",
year        = 2000,
month       = sep}

@article{wand79,
author = "Mitchell Wand",
title = "Final Algebra Semantics and Data Type Extension",
year = 1979,
journal = "Journal of Computer and System Sciences",
volume = 19,
pages = "27--44"}

@book{waerden85,
title = "A History of Algebra",
author = "Bartel van der Waerden",
year = 1985,
publisher = "Springer"}

@book{boyer-moore,
title = "A Computational Logic Handbook",
author = "R.S. Boyer and J.S. Moore",
year = 1998,
publisher = "Academic Press"}

@article{wand80,
author = "Mitchell Wand",
title = "First-Order Identities as a Defining Language",
journal = "Acta Informatica",
volume = 14,
pages = "337--357",
year = 1980}

@article{wand80-fsh,
author = "M. Wand",
title = "First-Order Identities as a Defining Language",
journal = "Acta Informatica",
volume = 14,
pages = "337--357",
year = 1980}

@book{wechler92,
author = "Wolfgang Wechler",
title = "Universal Algebra for Computer Scientists",
publisher = "Springer",
address = "Berlin",
year = "1992",
descriptor =   "Universelle Algebra"}

@book{whitehead98,
title = "A Treatise on Universal Algebra with Applications, I",
author = "Alfred North Whitehead",
publisher = "Cambridge",
year = 1898,
note = "Reprinted 1960"}

@incollection{whittle-etal01,
title = "{Amphion/NAV: Deductive Synthesis of State Estimation Software}",
author = "Jonathan Whittle and Jeff van Baalen and Johann Schumann and
  Peter Robinson and Thomas Pressburger and John Penix and Phil Oh and
  Michael Lowry and Guillaume Brat",
booktitle = "Proceedings, International Conference on
  Automated Software Engineering (ASE'01)",
publisher = "Institute of Electrical and Electronics Engineers",
year = 2001,
pages = "395--399",
note = "Coronado Island, California"}

@techreport{worrel97,
author = "James Worrell",
title = "A Topos of Hidden Algebras",
year = 1997,
institution = "Programming Research Group, University of Oxford",
number = "PRG-TR-28-97"}

@misc{yukawa90,
title = "The Untyped Lambda Calculus as a Logical Programming Language",
author = "Keitaro Yukawa",
year = 1990,
note = "City University of New York"}

@article{mes-RewLogFramework,
  author    = {Narciso Mart\'{\i}-Oliet and
               Jos{\'e} Meseguer},
  title     = {Rewriting logic as a logical and semantic framework},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {4},
  year      = {1996},
}


@article{bryant-ieeetc86,
author = "Randal E. Bryant",
title = "Graph-Based Algorithms for {B}oolean Function Manipulation",
journal = ieeetc,
volume = "C-35",
number = 8,
monthXXX = aug,
year = 1986,
pages = "677--691"}

@incollection{klop92term,
author = "J. W. Klop",
title = "Term Rewriting Systems",
booktitle = "Handbook of Logic in Computer Science,
  Volumes 1 (Background: Mathematical Structures) and
          2 (Background: Computational Structures)",
publisher = "Clarendon",
volume = "2",
year = "1992"}

@article{WalickiMeldal1997-fsh,
author = "M. Walicki and S. Meldal",
title = "Algebraic Approaches to Nondeterminism: An overview",
journal = "ACM Computing Surveys",
volume = 29,
pages = "30--81",
year = 1997}


@article{dim-gen, author = {Theodosis Dimitrakos and Tom Maibaum}, title = {On a generalised modularization theorem.}, journal = {Inf. Process. Lett.}, volume = {74}, number = {2}, year = {2000}, pages = {65--71}}

@inproceedings{mcm-int,
author = "Kenneth L. McMillan",
title = "Interpolation and sat-based model checking",
booktitle = "Computed Aided Verification 2003",
pages = "1--13",
year = "2003",
series = "LNCS",
volume = "2725",
publisher = "Springer"}


@inproceedings{mcm-int2, author = {Kenneth L. McMillan}, title = {An Interpolating Theorem Prover}, booktitle = {TACAS}, year = {2004}, pages = {16--30}, volume=2988, pages="16--30" }

@article{nel-sim,
 author = {Greg Nelson and Derek C. Oppen},
 title = {Simplification by Cooperating Decision Procedures},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {1},
 number = {2},
 year = {1979},
 pages = {245--257}
 }

@article{opp-com,
 author = {Derek C. Oppen},
 title = {Complexity, convexity and combinations of theories},
 journal = {Theor.\ Comput.\ Sci.},
 volume = {12},
 year = {1980},
 pages = {291--302}
  }

@inproceedings{tin-com,   author = "Cesare Tinelli and  Calogero Zarba",   title = "Combining Decision Procedures for Sorted Theories",   editor = "Alferes, Jos{\'e} J{\'u}lio and   Leite, Jo{\~a}o Alexandre",   booktitle = "Logics in Artificial Intelligence",   volume = "3229",   series = "LNCS",   pages = "641--653",   publisher = "Springer",   year = "2004"}


@article{bor-log, author = {Tomasz Borzyszkowski}, title = {Logical systems for structured specifications.}, journal = {Theor. Comput. Sci.}, volume = {286}, number = {2}, year = {2002}, pages = {197--245} }

@article{bor-gen, author = {Tomasz Borzyszkowski}, title = {Generalized interpolation in {CASL}.}, journal = {Inf. Process. Lett.}, volume = {76}, number = {1-2}, year = {2000}, pages = {19--24}}

@article{dia-int, author = {Razvan Diaconescu}, title = {Interpolation in {G}rothendieck Institutions.}, journal = {Theor. Comput. Sci.}, volume = {311}, year = {2004}, pages = {439--461} }

@article{mad-int, author = {Judit X. Madar{\'a}sz}, title = {Interpolation and Amalgamation; {P}ushing the Limits. {P}art II.}, journal = {Studia Logica}, volume = {62}, number = {1}, year = {1999}, pages = {1--19} }

@inproceedings{weich-decProcIntProp,
  author    = {Klaus Weich},
  title     = {Decision Procedures for Intuitionistic Propositional Logic
               by Program Extraction},
  booktitle = {TABLEAUX},
  year      = {1998},
  pages     = {292--306}
}

@inproceedings{and-cra,   author = "Hajnal Andr\'{e}ka and Istv\'{a}n N\'{e}meti and  Ildik\'{o} Sain",   title = "Craig Property of a Logic and Decomposability of Theories",   editor = "P. Dekker and M. Stokhof",   booktitle = "Proceedings of the Ninth Amsterdam Colloquium",   volume = "3229",   series = "LNCS",   year ={1993}, pages = "87--93"}
@article{bic-int, title = {Interpolation in Practical Formal Development}, author = {J. Bicarregui, T. Dimitrakos, D. Gabbay and T. Maibaum}, pages = {231--243}, volume = {9}, number = {1}, year = {2001}, journal = {Logic Journal of the IGPL} }
@article{dia-ele, author = {R\u{a}zvan Diaconescu}, title = {Elementary diagrams in institutions}, journal = {Journal of Logic and Computation}, year = 2004, volume = 14, number = 5, pages = "651--674" }

@incollection{kripke-com-revisited,
author = "Sarah Negri",
title = "Kripke completeness revisited",
year = 2009,
booktitle = "Acts of Knowledge---History, Philosophy and Logic",
publisher = "College Publications, London",
pages = "247--282",
editor = "G. Primiero and S. Rahman"}

@article{Kripke_1959, title={A Completeness Theorem in Modal Logic}, volume={24}, 
number={1}, journal={J. Symb.\ Log.}, publisher={JSTOR}, author={Kripke, S}, year={1959}, pages={1--14}}

@book{mon-mat,
title = "Mathematical Logic",
author = "J. Donald Monk",
publisher = "Springer",
year = 1976}

@book{fitting-FOL,
title = "First-Order Logic and Automated Theorem Proving",
author = "Melvin Fitting",
publisher = "Springer",
year = 1996}

@book{bell-machover-course,
title = "A Course in Mathematical Logic",
author = "J. L. Bell and M. Machover",
publisher = "North-Holland",
year = 1977}

@book{bar-mod,
title = "Model-Theoretic Logics",
author = "J. Barwise and J. Feferman",
publisher = "Springer",
year = 1985}

@inproceedings{sai-bet, author = {Ildik{\'o} Sain}, title =
{Beth's and {C}raig's properties via epimorphisms and amalgamation in algebraic logic},
booktitle = {Algebraic Logic and Universal Algebra in Computer Science}, year = {1988}, pages = {209--225} }

@book{kei-mod,
title = "Model Theory for Infinitary Logic",
author = "H. J. Keisler",
publisher = "North-Holland",
year = 1971}

@article{dag-cha, author = {Giovanna D'Agostino},
title = {Characterizing Interpolation Pairs in Infinitary Graded Logics},
journal = {J. Log. Comput.}, volume = {13}, number = {2}, year = {2003}, pages = {173--193} }

@inproceedings{wir-str,   author = "Martin Wirsing",
  title = "Structured Specifications: Syntax, Semantics and Proof Calculus",
  editor = "F. L. Bauer and W. Bauer and H. Schwichtenburg",
  booktitle = "Logic and Algebra of Specification",   volume = "94",
  series = "NATO ASI Series F: Computer and System Sciences",   pages = "411--442",
  publisher = "Springer",   year = "1991"}

@book{Hardin:2010:DVM:1841184,
 author = {Hardin, David S.},
 title = {Design and Verification of Microprocessor Systems for High-Assurance Applications},
 year = {2010},
 edition = {1st},
 publisher = {Springer Publishing Company, Incorporated},
} 

@phdthesis{cen-for,
title =  "Formal Specifications with High-Order Parametrization",
author = "M. V. Cengarle",
school = "Institute for Informatics, Ludwig-Maximilians University, Munich",
year = "1994"}

@inproceedings{rob-res, author = {Abraham Robinson}, title = {A result on consistency and its application to
the theory of definition}, series = {Konikl. Ned. Akad. Wetenschap. (Amsterdam) Proc \{A\}}, volume = {59}, year = {1956}, pages = {47--58} }

@inproceedings{mos-wha,   author = "Till Mossakowski and Joseph Goguen and Razvan Diaconescu and Andrzej Tarlecki",   title = "What is a logic?",   editor = "Jean-Yves Beziau",   booktitle = "Logica Universalis",  pages = "113--133",   publisher = "Birkhauser",   year = "2005",
location="Montreaux, Switzerland"}




@unpublished{pau-godel,
author = "L. Paulson",
title = "A Mechanised Proof of {G}{\"o}del Incompleteness Theorems using {N}ominal {I}sabelle",
note = "\url{http://www.cl.cam.ac.uk/~lp15/papers/Sets}"}



@unpublished{gabbay-thesis,
author = "M. J. Gabbay",
title = "A theory of inductive definitions with $\alpha$-equivalence",
note = "Ph.D. thesis. University of Cambridge, 2001."}

@unpublished{dia-abs,
author = "Marius Petria and R\u{a}zvan Diaconescu",
title = "Abstract {B}eth definability institutionally",
note = "Submitted.  (Ask authors for current version at {R}azvan.{D}iaconescu@imar.ro)"}

@unpublished{dia-pro,
author = "R\u azvan Diaconescu",
title = "Institutions with proofs",
note = "Submitted.  (Ask author for current version at {R}azvan.{D}iaconescu@imar.ro)"}


@article{dia-her, author = {R\u{a}zvan Diaconescu}, title = {Herbrand Theorems in arbitrary institutions}, journal = {Inf. Process. Lett.}, volume = {90}, year = {2004}, pages = {29--37} }

@book{san-car,
author = "Don Sannella and Andrzej Tarlecki",
title = "Foundations of Algebraic Specifications and Formal Program Development", publisher = {Cambridge University Press},
note = "To appear.  (Ask authors for current version at tarlecki@mimuw.edu.pl)"}

@book{mak-acc,
author = "Michael Makkai and Robert Par\'{e}",
title = "Accessible Categories: The Foundations of Categorical Model Theory", publisher = {Providence},
location = "Rhode Island",
year = "1989"}

@book{sac-sat,
author = "Gerald E. Sacks",
title = "Saturated Model Theory", publisher={W. A. Bejamin, Inc., Reading},
location = "Massachusetts",
year = "1972"}

@article{hir-for,
author = "J. Hirschfeld and W. Wheeler",
title = "Forcing, arithmetic, division rings", journal = {Lecture Notes in Mathematics}, number = {454}, year = {1975}}

@article{mak-fir, author = {Michael Makkai and G. E. Reyes}, title = {First Order Categorical Logic},
journal = {Lecture Notes in Mathematics}, number = {611}, year = {1977}}

@article{gog-int,
author = "Rod Burstall and Joseph Goguen",
title = "Semantics of {C}lear",
note = "Unpublished notes handed out at the 1978 Symposium on Algebra and Applications.
Stefan Banach Center, Warsaw, Poland, 1978" }

@article{mun-rob1, author = {Daniele Mundici}, title = {Robinson Consistency Theorem
in Soft Model Theory},
journal = {Atti Accad. Nat. Lincei.  Redingoti}, volume ={67}, year = {1979}, pages={383--386}}

@article{mun-rob2, author = {Daniele Mundici}, title = {Robinson's Consistency Theorem
in Soft Model Theory},
journal = {Trans. of the AMS}, volume ={263}, year = {1981}, pages={231--241}}

@unpublished{mun-com,
author = "Daniele Mundici",
title = "Compactness $+$ {C}raig Interpolation $=$ {R}obinson Consistency in any logic",
year="1979",
note = "Manuscript.  University of Florence"}


@unpublished{clinger-actors,
author = "William Clinger",
title = "Foundations of Actor Semantics",
year="1981",
note = "Mathematics Doctoral Dissertation. MIT"}


@unpublished{wei-cou,
author = "W. A. R. Weiss and Cherie D'Mello",
title = "Fundamentals of Model Theory",
year="1997",
note = "Lecture Notes, University of Toronto."}

@inproceedings{fef-lec,   author = "S. Feferman",   title = "Lectures on proof theory",   editor = "M. H. Lob",   booktitle = "Proceedings of the Summer School in Logic, Lecture Notes in Mathematics",  pages = "1--107",  volume = "70",
year = "1968",
location="Leeds"}

@article{kri-com,
title = "A completeness theorem in modal logic",
author = "Saul Kripke",
year = 1959,
journal = "J. Symb. Log.",
volume = 24, pages = "1--15"}


@inproceedings{keiko1,
  author    = {Keiko Nakata and
               Tarmo Uustalu},
  title     = {Trace-Based Coinductive Operational Semantics for While},
  booktitle = {TPHOLs},
  year      = {2009},
  pages     = {375--390},
}


@article{keiko2,
  author    = {Keiko Nakata and
               Tarmo Uustalu},
  title     = {Resumptions, Weak Bisimilarity and Big-Step Semantics for
               While with Interactive I/O: An Exercise in Mixed Induction-Coinduction},
  journal   = {CoRR},
  volume    = {abs/1008.2112},
  year      = {2010},
}


@inproceedings{keiko3,
  author    = {Keiko Nakata and
               Tarmo Uustalu},
  title     = {A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics
               of While},
  booktitle = {ESOP},
  year      = {2010},
  pages     = {488--506},
}





@incollection{bur-hid,
author = "Rod Burstall and R\u{a}zvan Diaconescu",
title = "Hiding and behaviour: an institutional approach",
year = 1994,
booktitle = "A Classical Mind: Essays in Honour of C. A. R. Hoare",
publisher = "Prentice-Hall",
pages = "75--92",
editor = "A. William Roscoe"}

@book{gal-log,
author = {Jean H. Gallier},
title = {Logic for Computer Science---Foundations of Automatic Theorem Proving},
publisher = "Harper \& Row",
series = "Computer Science and Technology",
year = 1986}


@book{francez-fairness,
  author = {Nissim Francez},
  title = {Fairness},
  series    = {Texts and Monographs in Computer Science},
  publisher = "Springer",
  year = 1986}

@unpublished{tra-mas,
  author = "Traian {\c S}erb\u{a}nu\c{t}\u{a}",
  title = "Institutional concepts in first-order logic, parameterized specifications, and logic programming.",
  note = "Master Disertation.  University of Bucharest, 2004."}


@article{aba-exp,
author = {Mart\'{\i}n Abadi and Luca Cardelli and Pierre-Louis Curien and Jean-Jacques L{\'e}vy},
title = {Explicit Substitutions},
journal = {J.~Funct. Program.},
volume = {1},
 number = {4},
year = {1991},
pages = {375--416}}


@inproceedings{weakHOASInd,
 author = {Jo\"{e}lle Despeyroux and Andr\'{e} Hirschowitz},
 title = {Higher-Order Abstract Syntax with Induction in Coq},
 booktitle = {LPAR '94: Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning},
 year = {1994},
 pages = {159--173}
 }


@article{GrooteStructOpSemBisim,
 author = {Jan Friso Groote and Frits Vaandrager},
 title = {Structured operational semantics and bisimulation as a congruence},
 journal = {Inf. Comput.},
 volume = {100},
 number = {2},
 year = {1992},
 pages = {202--260},
 }

@book{andrews-2002,
 author = {Peter B. Andrews},
 title = {An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof},
 edition = "2nd",
 series = "Applied Logic",
 volume = {27},
 year = {2002},
 publisher = {Springer}
}

@book{gordon-melham-1993,
  editor = "M. J. C. Gordon and T. F. Melham",
  title = "Introduction to {HOL}: A~Theorem Proving Environment for Higher Order
Logic",
  publisher = "Cambridge University Press",
  year = 1993}

@inproceedings{harrison-1996,
  author = "John Harrison",
  title = "{HOL} {L}ight: A Tutorial Introduction",
  booktitle = "FMCAD '96",
  publisher = "Springer",
  series = "LNCS",
  volume = "1166",
  pages = "265--269",
  year = 1996}

@inproceedings{wadler-89,
  author    = {Philip Wadler},
  title     = {Theorems for Free!},
  booktitle = {FPCA '89},
  year      = {1989},
  pages     = {347--359},
  publisher = "ACM"
}

@inproceedings{adams-2010,
  author    = {Mark Adams},
  title     = {Introducing {HOL Zero} (Extended Abstract)},
  booktitle = {ICMS '10},
  year      = {2010},
  pages     = {142--143},
  editor    = {Komei Fukuda and
               Joris van der Hoeven and
               Michael Joswig and
               Nobuki Takayama},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6327}
}

@inproceedings{arthan-2004,
  author = "R. D. Arthan",
  title = "Some Mathematical Case Studies in {P}roof\-{P}ower--{HOL}",
  booktitle = "TPHOLs 2004 (Emerging Trends)",
  editor = "Konrad Slind",
  pages = "1--16",
  year = 2004}

@misc{crow-et-al-1995,
  author = "Judy Crow and Sam Owre and John Rushby and Natarajan Shankar and Mandayam Srivas",
  title = "A~Tutorial Introduction to {PVS}",
  howpublished = "WIFT '95",
  year = "1995"}

@inproceedings{backes-brown-2010,
  title = "Analytic Tableaux for Higher-Order Logic with Choice",
  author = "Julian Backes and Chad E. Brown",
  booktitle = "IJCAR '10",
  editor = {J\"urgen Giesl and Reiner H\"ahnle},
  publisher="Springer",
  series={{LNAI}},
  volume = 6173,
  pages = "76--90",
  year = 2010}

@inproceedings{benzmueller-et-al-2008-leo2,
  author = "Christoph Benzm{\"u}ller and Lawrence C. Paulson and Frank Theiss and Arnaud Fietzke",
  title = "{LEO-II}---{A} Cooperative Automatic Theorem Prover for Higher-Order Logic",
  editor = "Alessandro Armando and Peter Baumgartner and Gilles Dowek",
  booktitle = "IJCAR '08",
  publisher="Springer",
  series={{LNAI}},
  volume = 5195,
  pages = "162--170",
  year = 2008}

@inproceedings{voelker-2007,
  author    = {Norbert V{\"o}lker},
  title     = {{HOL2P}---{A} System of Classical Higher Order Logic with Second
               Order Polymorphism},
  booktitle = {TPHOLs 2007},
  year      = {2007},
  pages     = {334--351},
  editor    = {Klaus Schneider and
               Jens Brandt},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4732}
}

@inproceedings{homeier-2009,
  author    = {Peter V. Homeier},
  title     = {The {HOL-Omega} Logic},
  booktitle = {TPHOLs 2009},
  year      = {2009},
  pages     = {244--259},
  editor    = {Stefan Berghofer and
               Tobias Nipkow and
               Christian Urban and
               Makarius Wenzel},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5674},
}

@inproceedings{reif-et-al-1997,
  author    = {Wolfgang Reif and
               Gerhard Schellhorn and
               Kurt Stenzel},
  title     = {Proving System Correctness with {KIV} 3.0},
  booktitle = {CADE-14},
  year      = {1997},
  pages     = {69--72},
  editor    = {William McCune},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {1249},
}

@inproceedings{siekmann-et-al-2003,
  author = "J{\"o}rg Siekmann and Christoph Benzm{\"u}ller and Armin Fiedler and Andreas Meier and Immanuel Normann and Martin Pollet",
  title = "Proof Development with {\OMEGA}: The Irrationality of {$\sqrt2$}",
  editor = "Fairouz Kamareddine",
  booktitle = "Thirty Five Years of Automating Mathematics",
  series = "Applied Logic",
  volume = {28},
  pages = "271--314",
  year = 2003,
  publisher = "Springer"}
%%% HACK: TYPESETTING: Thirty Five

@inproceedings{gunter-1993-not,
  author    = {Elsa L. Gunter},
  title     = {Why we can't have {SML}-style \texttt{datatype} Declarations in {HOL}},
  booktitle = {TPHOLs '92},
  pages     = {561--568},
  editor    = {Luc J. M. Claesen and
               Michael J. C. Gordon},
  publisher = {North-Holland/Elsevier},
  series    = {IFIP Transactions},
  volume    = {A-20},
  year      = {1993}
}

@article{containers,
  author    = {Michael Abbott and
               Thorsten Altenkirch and
               Neil Ghani},
  title     = {Containers: Constructing strictly positive types},
  journal   = {Theor. Comput. Sci.},
  volume    = {342},
  number    = {1},
  year      = {2005},
  pages     = {3--27}
}

@article{containerTypesCat,
  author    = {Paul F. Hoogendijk and
               Oege de Moor},
  title     = {Container types categorically},
  journal   = {J.~Funct. Program.},
  volume    = {10},
  number    = {2},
  year      = {2000},
  pages     = {191--225}
}

@inproceedings{indexedContainers,
  author    = {Thorsten Altenkirch and
               Peter Morris},
  title     = {Indexed Containers},
  booktitle = {LICS 2009},
  year      = {2009},
  pages     = {277--285},
  publisher = "IEEE"
}


@inproceedings{gunter-1994-trees,
  author    = {Elsa L. Gunter},
  title     = {A Broader Class of Trees for Recursive Type Definitions
               for {HOL}},
  booktitle = {HUG '93},
  pages     = {141--154},
  editor    = {Jeffrey J. Joyce and
               Carl-Johan H. Seger},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {780},
  year      = {1994}
}

@inproceedings{slind-norrish-2008,
    author = {Konrad Slind and Michael Norrish},
    booktitle = {TPHOLs 2008},
    editor = "Otmane Ait Mohamed and C\'esar Mu{\~n}oz and
Sofi\`ene Tahar",
    title = {A Brief Overview of {HOL4}},
    pages = {28--32},
    publisher = "Springer",
    series = {{LNCS}},
    volume = {5170},
    year = {2008}}

@inproceedings{DBLP:conf/tlca/Bertot05,
  author    = {Yves Bertot},
  title     = {Filters on CoInductive Streams, an Application to {E}ratosthenes'
               Sieve},
  booktitle = {TLCA 2005},
  year      = {2005},
  pages     = {102--115}
}


@inproceedings{berghofer-wenzel-1999,
    author = {Stefan Berghofer and Markus Wenzel},
    booktitle = {TPHOLs '99},
    title = {Inductive Datatypes in {HOL}---{L}essons Learned in Formal-Logic Engineering},
editor = {Yves Bertot and Gilles Dowek and Andr\'e Hirschowitz and Christine Paulin
and Laurent Th\'ery},
pages = {19--36},
    series = {{LNCS}},
    volume = {1690},
    year = {1999}}

@inproceedings{huffman-2009,
  author    = {Brian Huffman},
  title     = {A Purely Definitional Universal Domain},
  booktitle = {TPHOLs 2009},
  year      = {2009},
  pages     = {260--275},
  editor    = {Stefan Berghofer and
               Tobias Nipkow and
               Christian Urban and
               Makarius Wenzel},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5674}
}

@book{gordon-et-al-1979,
  author = "Michael J. C. Gordon and Robin Milner and Christopher P. Wadsworth",
  title = "Edinburgh {LCF}: A Mechanised Logic of Computation",
  series = "LNCS",
  volume = 78,
  publisher = "Springer",
  year = 1979}

@incollection{melham-1989,
  AUTHOR = {Thomas F. Melham},
  TITLE = {Automating Recursive Type Definitions in
                   Higher Order Logic},
  BOOKTITLE = {Current Trends in Hardware Verification and
                   Automated Theorem Proving},
  editor = {G. Birtwistle and P. A. Subrahmanyam},
  PUBLISHER = {Springer},
  YEAR = {1989},
  PAGES = {341--386},
}

@inproceedings{harrison-1995,
  author = "John Harrison",
  title = "Inductive Definitions: Automation and Application",
  booktitle = "TPHOLs '95",
  editor = {E. Thomas Schubert and Phillip J. Windley and Jim Alves-Foss},
  publisher = "Springer",
  series = "LNCS",
  volume = "971",
  pages = "200--213",
  year = 1995}

@article{paulson-1997,
  author    = {Lawrence C. Paulson},
  title     = {Mechanizing Coinduction and Corecursion in Higher-Order
               Logic},
  journal   = {J. Log. Comput.},
  volume    = {7},
  number    = {2},
  year      = {1997},
  pages     = {175--204}
}

@article{lochbihler-AFP-2010,
  author =   {Andreas Lochbihler},
  title =    {Coinductive},
  journal =  {Archive of Formal Proofs},
  month =    Feb,
  year =     2010,
  note =     {\url{isa-afp.org/entries/Ordinals_and_Cardinals.shtml}, Formal proof development},
}

@article{popescu-2009-AFP,
  author =   {Andrei Popescu},
  title =    {Ordinals and Cardinals},
  journal =  {Archive of Formal Proofs},
  month =    "March",
  year =     2009,
  note =     {\url{http://isa-afp.org/entries/Coinductive.shtml}, Formal proof development},
}

@article{andrews-et-al-1996,
  author = {Peter B. Andrews and Matthew Bishop and Sunil Issar and Dan Nesmith and Frank Pfenning and Hongwei Xi},
  title = {{TPS}: A Theorem-Proving System for Classical Type Theory},
  journal = {J.~Autom.\ Reasoning},
  volume = 16,
  number = 3,
  pages = {321--353},
  year = 1996}

@inproceedings{homeier-2005,
  author    = {Peter V. Homeier},
  title     = {A Design Structure for Higher Order Quotients},
  booktitle = {TPHOLs 2005},
  pages     = {130--146},
  editor    = {Joe Hurd and
               Thomas F. Melham},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {3603},
  year      = {2005}
}

%  day = 18,
@misc{homeier-2011-email,
  author = "Peter Vincent Homeier",
  title = "Abstract data types in {HOL-O}mega",
  month = "18 Apr.",
  year = 2011,
  howpublished = "\url{http://permalink.gmane.org/gmane.comp.mathematics.hol/1168}"}

@inproceedings{kaliszyk-urban-2011,
  title = "Quotients Revisited for {I}sabelle\slash {HOL}",
  author = "Cezary Kaliszyk and Christian Urban",
  booktitle = "SAC '11",
  editor    = {William C. Chu and
               W. Eric Wong and
               Mathew J. Palakal and
               Chih-Cheng Hung},
  pages = "1639--1644",
  publisher = "ACM",
  year = 2011}

@article{mueller-et-al-1999,
  author = {Olaf M\"uller and Tobias Nipkow and von Oheimb, David and Oskar Slotosch},
  title={{HOLCF = HOL + LCF}},
  journal={J.~Funct. Program.},
  volume=9,
  pages={191--223},
  year=1999}

@misc{voelker-1995,
  author = {N. V\"olker},
  title = "On the representation of datatypes in {Isabelle\slash HOL}",
  howpublished = "Isabelle Users Workshop",
  year = 1995}

@inproceedings{huffman-urban-2010,
  author    = {Brian Huffman and
               Christian Urban},
  title     = {Proof Pearl: A New Foundation for {Nominal Isabelle}},
  booktitle = {ITP '10},
  year      = {2010},
  pages     = {35--50},
  editor    = {Matt Kaufmann and
               Lawrence C. Paulson},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6172}
}

@article{urban-2008,
  author    = {Christian Urban},
  title     = {Nominal Techniques in {Isabelle\slash HOL}},
  journal   = {J. Autom. Reasoning},
  volume    = {40},
  number    = {4},
  year      = {2008},
  pages     = {327--356}
}

@misc{vos-swierstra-2002,
  author = "Tanja E. J. Vos and S. Doaitse Swierstra",
  title = "Inductive Data Types with Negative Occurrences in {HOL}",
  year = "2002",
  howpublished = "Thirty Five Years of Automath"}
%%% HACK: TYPESETTING: Thirty Five

@article{sasse-meseguer-2007,
  author    = {Ralf Sasse and
               Jos{\'e} Meseguer},
  title     = {{J}ava+{ITP}: A Verification Tool Based on {H}oare Logic and Algebraic
               Semantics},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {176},
  number    = {4},
  year      = {2007},
  pages     = {29--46}
}

@article{clavel-et-al-1996,
  author    = {Manuel Clavel and
               Steven Eker and
               Patrick Lincoln and
               Jos{\'e} Meseguer},
  title     = {Principles of {M}aude},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {4},
  year      = {1996},
  pages     = {65--89}
}

@techreport{owre-shankar-1993,
  author = "S. Owre and N. Shankar",
  title = "Abstract datatypes in {PVS}",
  number = "CSL-93-9R",
  institution = "C.S.\ Lab., SRI International",
  year = 1993,
}
%%% HACK: TYPESETTING:  note = "Revised 1997"

@inproceedings{gottliebsen-2004,
  author = "Hanne Gottliebsen",
  title = "Co-inductive Proofs for Streams in {PVS}",
  booktitle = "TPHOLs 2007 (Emerging Trends)",
  editor = "Klaus Schneider and Jens Brandt",
  pages = "113--127",
  year = 2007}

@article{paulson-1993-zf,
  author = "Lawrence C. Paulson",
  title = "Set Theory for Verification: {I}.\ {F}rom foundations to functions",
  journal = {J.~Autom.\ Reasoning},
  volume = 11,
  number = 3,
  pages = "353--389",
  year = 1993}

@article{paulson-1995-zf,
  author = "Lawrence C. Paulson",
  title = "Set theory for verification: {II}.\ {I}nduction and recursion",
  journal = {J.~Autom.\ Reasoning},
  volume = 15,
  number = 2,
  pages = "167--215",
  year = 1995}

%%% TODO: CHECK title and booktitle
@inproceedings{rosu-2006-icfp,
title={Equality of Streams is a \smash{$\Pi_2^0$}-Complete Problem},
author={Grigore Ro\c{s}u},
booktitle={ICFP~{'}06},
publisher={ACM},
year="2006"
}

@inproceedings{paulson-1994,
  author    = {Lawrence C. Paulson},
  title     = {A Concrete Final Coalgebra Theorem for {ZF} Set Theory},
  booktitle = {TYPES~'94},
  pages     = {120--139},
  editor    = {Peter Dybjer and
               Bengt Nordstr{\"o}m and
               Jan M. Smith},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {996},
  year      = {1995}
}

@inproceedings{nakata-et-al-2011,
  author    = {Keiko Nakata and
               Tarmo Uustalu and
               Marc Bezem},
  title     = {A Proof Pearl with the Fan Theorem and Bar Induction---{W}alking
               through Infinite Trees with Mixed Induction and Coinduction},
  booktitle = {APLAS 2011},
  year      = {2011},
  pages     = {353--368},
  editor    = {Hongseok Yang},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {7078}
}

@book{bertot-casteran-2004,
  title = "Interactive Theorem Proving and Program Development---{Coq'Art}: The Calculus of Inductive Constructions",
  series = "Texts in Theoretical Computer Science",
  publisher = "Springer",
  author = "Bertot, Yves and Cast\'eran, Pierre",
  year = 2004}

@inproceedings{DBLP:conf/itp/BlanchettePWW12,
  author    = {Jasmin Christian Blanchette and
               Andrei Popescu and
               Daniel Wand and
               Christoph Weidenbach},
  title     = {More {SPASS} with {I}sabelle - Superposition with Hard Sorts
               and Configurable Simplification},
  booktitle = {ITP},
  year      = {2012},
  pages     = {345-360}
}

@ARTICLE{sabelfel-lb-security,
author={Sabelfeld, Andrei and Myers, Andrew C.},
journal={IEEE Journal on Selected Areas in Communications},
title={Language-based information-flow security},
year={2003},
volume={21},
number={1},
pages={ 5--19}
}

@inproceedings{bove-et-al-2009,
  author    = {Ana Bove and
               Peter Dybjer and
               Ulf Norell},
  title     = {A Brief Overview of {A}gda---{A} Functional Language with Dependent
               Types},
  booktitle = {TPHOLs 2009},
  year      = {2009},
  pages     = {73--78},
  editor    = {Stefan Berghofer and
               Tobias Nipkow and
               Christian Urban and
               Makarius Wenzel},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5674}
}

@inproceedings{DBLP:conf/icse/Leino04,
  author    = {K. Rustan M. Leino},
  title     = {Developing verified programs with {D}afny},
  booktitle = {ICSE},
  year      = {2013},
  pages     = {1488-1490}
}

@misc{our-development,
  author = "Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel",
  title = "Formal development associated with this paper",
  howpublished = "\url{http://www21.in.tum.de/~popescua/compl_devel.zip}",
  year = 2013
}

@misc{cocon-formalization-2014,
  author = "Andrei Popescu and Peter Lammich",
  title = "Verification of {C}o{C}on---formal {I}sabelle development",
  howpublished = "\url{http://www21.in.tum.de/~popescua/rs3/cocon-form-2014.zip}",
  year = 2013
}

@misc{rs3,
  title = "Reliably Secure Software Systems ({RS}$^3$)",
  howpublished = "\url{http://www.reliably-secure-software-systems.de}",
  year = 2013
}

@misc{secded-project,
  title = "Security Type Systems and Deduction---project affiliated to {RS}$^3$",
  howpublished = "\url{http://www21.in.tum.de/~popescua/rs3/secded.html}",
  year = 2013
}

@misc{larger-devel,
  author = "Jasmin Christian Blanchette and Andrei Popescu",
  title = "Formalization of the metatheory of {M}any-{S}orted {F}irst-{O}rder {L}ogic",
  howpublished = "\url{http://www21.in.tum.de/~popescua/MFOL_devel.zip}",
  year = 2013
}

@incollection{traytel-et-al-2012,
  author = "Dmitriy Traytel and Andrei Popescu and Jasmin Christian Blanchette",
  title     = {Foundational, Compositional (Co)datatypes for Higher-Order
               Logic---{C}ategory Theory Applied to Theorem Proving},
  year      = {2012},
  pages     = {596--605},
  booktitle = {LICS}
}


@inproceedings{pop-prob,
  author    = {Andrei Popescu and
               Johannes H{\"o}lzl and
               Tobias Nipkow},
  title     = {Formalizing Probabilistic Noninterference},
  booktitle = {CPP},
  year      = {2013},
  pages     = {259-275}
}


@unpublished{mizar-hammer,
  author = "P. Rudnicki and J. Urban",
  title = "Escape to {ATP} for {M}izar",
  note = "PxTP 2011"
}

@misc{scala,
title = "The {S}cala {P}rogramming {L}anguage",
note = "\url{http://www.scala-lang.org}",
year = "2014"}

@inproceedings{agat,
  author    = {Johan Agat},
  title     = {Transforming Out Timing Leaks},
  booktitle = {POPL},
  year      = {2000},
  pages     = {40-53}
}

@techreport{rushby-nonint,
    AUTHOR = {John Rushby},
    TITLE = {Noninterference, Transitivity, and Channel-Control Security Policies},
    YEAR = {1992},
    MONTH = {dec},
    URL = {http://www.csl.sri.com/papers/csl-92-2/},
    BOOKTITLE = {Technical Report {CSL-92-02}}
}

@inproceedings{DBLP:conf/sp/GoguenM84,
  author    = {Joseph A. Goguen and
               Jos{\'e} Meseguer},
  title     = {Unwinding and Inference Control},
  booktitle = {IEEE Symposium on Security and Privacy},
  year      = {1984},
  pages     = {75-87}
}

@unpublished{topic-workshop,
  author = "Thomas Bauerei\ss and 
Christoph Feller and 
Peter Lammich and 
Steffen Lortz and 
M\'at\'e Kov\'acs and  
Mart\'in Ochoa and 
Andrei Popescu and 
Markus N. Rabe",
  title = "Formal Verification of Information Flow Properties of Web-Based Workflow Management Systems -- Topic Workshop Report",
  note = "Available at \url{http://www21.in.tum.de/~popescua/topic-workshop.pdf}"
}

@unpublished{ref-scen,
  author = "IFC4BC and IFC4MC and MORES and SecDed and SpAGAT",
  title = "Security in Web-Based Workflow Management Systems -- {RS}$^3$ Reference Scenario Report",
  note = "Available at \url{http://www21.in.tum.de/~popescua/rs3/ref-scen-2014.pdf}"
}

@unpublished{CoCon,
  author = "Sudeep Kanav and Peter Lammich and Andrei Popescu",
  title = "The {CoCon} Website",
  note = "\url{http://www21.in.tum.de/~popescua/rs3/GNE.html}"
}



@article{DBLP:journals/corr/abs-1211-7012,
  author    = {Cezary Kaliszyk and
               Josef Urban},
  title     = {Learning-assisted Automated Reasoning with {F}lyspeck},
  journal   = {CoRR},
  volume    = {abs/1211.7012},
  year      = {2012}
}

@inproceedings{sutherland-modelOfInf,
  author    = {D. Sutherland},
  title     = {A Model of Information},
  booktitle = {9th National Security Conference},
  year      = {1986},
  pages     = {175--183}
}

@unpublished{mcbride-productive,
  author = "Robert Atkey and Conor McBride",
  title = "Productive Coprogramming with Guarded Recursion",
  note = "To appear in ICFP 2013."
}

@article{DBLP:journals/afp/Blanchette013,
  author    = {Jasmin Christian Blanchette and
               Andrei Popescu},
  title     = {Sound and Complete Sort Encodings for First-Order Logic},
  journal   = {Archive of Formal Proofs},
  year      = {2013}
}

@article{bdsec-afp,
  author    = {Andrei Popescu and Peter Lammich},
  title     = {Bounded-Deducibility Security},
  journal   = {Archive of Formal Proofs},
  year      = {2014}
}

@article{hyperCTL-in-Isabelle,
  author    = {Markus N. Rabe and Peter Lammich and Andrei Popescu},
  title     = {A shallow embedding of {H}yper{CTL}$^*$},
  journal   = {Archive of Formal Proofs},
  year      = {2014}
}

@article{DBLP:journals/afp/HolzlN12,
  author    = {Johannes H{\"o}lzl and
               Tobias Nipkow},
  title     = {Markov Models},
  journal   = {Archive of Formal Proofs},
  year      = {2012}
}

@article{afp-possib,
  author    = {Andrei Popescu and
               Johannes H{\"o}lzl},
  title     = {Possibilistic Noninterference},
  journal   = {Archive of Formal Proofs},
  year      = {2012}
}

@article{afp-probab,
  author    = {Andrei Popescu and
               Johannes H{\"o}lzl},
  title     = {Probabilistic Noninterference},
  journal   = {Archive of Formal Proofs},
  year      = {2014}
}

@incollection{DBLP:series/ais/Smith07,
  author    = {Geoffrey Smith},
  title     = {Principles of Secure Information Flow Analysis},
  booktitle = {Malware Detection},
  year      = {2007},
  pages     = {291-307}
}


@unpublished{witCod-2013,
  author = "Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel",
  title = "Witnessing (co)datatypes",
  note = "Draft available at \url{http://www21.in.tum.de/~popescua/pdf/WIT.pdf}"
}

@unpublished{codatatype-doc,
  author = "Jasmin Christian Blanchette and Lorenz Panny and Andrei Popescu and Dmitriy Traytel",
  title = "Defining (co)datatypes in {I}sabelle/{HOL}",
  note = "Isabelle documentation \url{http://isabelle.in.tum.de/dist/Isabelle/doc/datatypes.pdf}", 
  year      = {2013}
}


@unpublished{confsys-2013,
  author = "Sudeep Kanav and Peter Lammich and Andrei Popescu",
  title = "A Conference Management System with Verified Document Confidentiality",
  note = "\url{http://www21.in.tum.de/~popescua/pdf/confsys.pdf}"
}

@unpublished{our-card-2013,
  author = "Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel",
  title = "Cardinals in {I}sabelle/{HOL}",
  note = "Draft available at \url{http://www21.in.tum.de/~popescua/pdf/card.pdf}"
}

@unpublished{impl-datatypes-2013,
  author = "Jasmin Christian Blanchette and Johannes H{\"o}lzl
  and Andreas Lochbihler and Lorenz Panny and Andrei Popescu and Dmitriy Traytel",
  title = "Truly Modular (Co)datatypes for {I}sabelle/{HOL}",
  note = "Draft available at \url{http://www21.in.tum.de/~popescua/pdf/codat-imp.pdf}"
}


@unpublished{complPearl-2013,
  author = "Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel",
  title = "Modular First-Order Logic Completeness for the Lazy Programmer",
  note = "Draft available at \url{http://www21.in.tum.de/~popescua/pdf/COMPL.pdf}"
}


@article{pop-jfr,
author = "Andrei Popescu and
               Johannes H{\"o}lzl and
               Tobias Nipkow",
  title = "Formal Verification of Language-Based Concurrent Noninterference",
journal = "Journal of Formalized Reasoning",
volume = 6,
year = 2013,
number = 1}

@inproceedings{pop-pos,
  author    = {Andrei Popescu and
               Johannes H{\"o}lzl and
               Tobias Nipkow},
  title     = {Proving Concurrent Noninterference},
  booktitle = {CPP},
  year      = {2012},
  pages     = {109-125}
}

@article{DBLP:journals/tcs/PopescuSR09,
  author    = {Andrei Popescu and
               Traian-Florin Serbanuta and
               Grigore Rosu},
  title     = {A semantic approach to interpolation},
  journal   = {Theor. Comput. Sci.},
  volume    = {410},
  number    = {12-13},
  year      = {2009},
  pages     = {1109-1128}
}

@incollection{popescu-2011-oc,
  title = "Ordinals and Cardinals in {HOL}",
  author = "Andrei Popescu and Dmitriy Traytel",
  publisher = "\url{http://www21.in.tum.de/~traytel/icfp13_card.tgz}",
  year = 2013
}

%  booktitle = "The Archive of Formal Proofs",
%  editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
%  publisher = "\url{isa-afp.org/release/afp-Ordinals_and_Cardinals-current.tar.gz}",
%  year = 2011
% or: isa-afp.org/browser_info/current/HOL/Ordinals_and_Cardinals/document.pdf

@incollection{lochbihler-2010-coinduction,
  author = "Andreas Lochbihler",
  booktitle = "The Archive of Formal Proofs",
  editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher = "\url{isa-afp.org/entries/Coinductive.shtml}",
  year = 2010}

@inproceedings{wenzel-wolff-2007,
  author    = {Makarius Wenzel and
               Burkhart Wolff},
  title     = {Building Formal Method Tools in the {Isabelle/Isar} Framework},
  booktitle = {TPHOLs 2007},
  pages     = {352--367},
  editor    = {Klaus Schneider and
               Jens Brandt},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4732},
  year      = {2007}
}

@article{DBLP:journals/corr/Popescu13,
  author    = {Andrei Popescu},
  title     = {Security Type Systems as Recursive Predicates},
  journal   = {CoRR},
  volume    = {abs/1308.3472},
  year      = {2013}
}

@phdthesis{traytel-2012,
  author = "Dmytro Traytel",
  title = "A Category Theory Based (Co)datatype Package for Isabelle\slash {HOL}",
  school = {TU~M\"unchen, 2012. \url{http://www21.in.tum.de/~traytel/mscthesis.pdf}},
  type = "{M.Sc.}\ thesis"}

@incollection{paulson-2000,
  author    = {Lawrence C. Paulson},
  title     = {A fixedpoint approach to (co)inductive and (co)datatype
               definitions},
  pages     = {187--212},
  editor    = {Gordon D. Plotkin and
               Colin Stirling and
               Mads Tofte},
  booktitle     = {Proof, Language, and Interaction---Essays in Honour of Robin
                   Milner},
  publisher = {MIT Press},
  year      = {2000}
}

@article{Hasegawa02,
  author    = {Ryu Hasegawa},
  title     = {Two applications of analytic functors},
  journal   = {Theor. Comput. Sci.},
  volume    = {272},
  number    = {1-2},
  year      = {2002},
  pages     = {113--175}
}

@article{pf-rev-gal,
  author    = {Frank Pfenning},
  title     = {Review of ``{Jean H. Gallier: Logic for Computer Science, Harper \& Row, New York 1986}'' \cite{gal-log}},
  journal   = {J. Symb. Log.},
  volume    = {54},
  number    = {1},
  year      = {1989},
  pages     = {288--289}
}

@article{DBLP:journals/fm/SchloderK12a,
  author    = {Julian J. Schl{\"o}der and
               Peter Koepke},
  title     = {The {G}{\"o}del Completeness Theorem for Uncountable Languages},
  journal   = {Formalized Mathematics},
  volume    = {20},
  number    = {3},
  year      = {2012},
  pages     = {199--203}
}

@article{kaplan-review-kripke,
  author    = {D. Kaplan},
  title     = {Review of {K}ripke (1959) \cite{Kripke_1959}},
  journal   = {J. Symb. Log.},
  volume    = {31},
  year      = {1966},
  pages     = {120--122}
}

@article{Ciaffaglione200639,
  author    = {Alberto Ciaffaglione and
               Pietro Di Gianantonio},
  title     = {A certified, corecursive implementation of exact real numbers},
  journal   = {Theor. Comput. Sci.},
  volume    = {351},
  number    = {1},
  year      = {2006},
  pages     = {39--51}
}

@inproceedings{rutten-regExp,
  author    = {Jan J. M. M. Rutten},
  title     = {Regular Expressions Revisited: A Coinductive Approach to
               Streams, Automata, and Power Series},
  booktitle = {MPC 2000},
  year      = {2000},
  pages     = {100--101}
}


@article{krauss-nipkow-2012,
  author    = {Alexander Krauss and
               Tobias Nipkow},
  title     = {Proof Pearl: Regular Expression Equivalence and Relation
               Algebra},
  journal   = {J. Autom. Reasoning},
  volume    = {49},
  number    = {1},
  year      = {2012},
  pages     = {95--106}
}

@misc{easychair,
key = "EasyChair",
title = "The {E}asy{C}hair Conference System",
note = "\url{http://easychair.org}",
year = "2014"}

@misc{hotCRP,
key = "EasyChair",
title = "The {H}ot{CRP} Conference System",
note = "\url{http://read.seas.harvard.edu/~kohler/hotcrp}"
%,
%year = "2014"
}

@inproceedings{lochbihler-2012,
  author    = {Andreas Lochbihler},
  title     = {{J}ava and the {J}ava Memory Model---{A} Unified, Machine-Checked
               Formalisation},
  booktitle = {ESOP 2012},
  year      = {2012},
  pages     = {497--517},
}

@inproceedings{EasyChair:227,
  author    = {Lawrence C. Paulson and Jasmin Christian Blanchette},
  title     = {Three years of experience with {S}ledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers},
  booktitle = {IWIL 2010},
  %editor    = {Geoff Sutcliffe and Stephan Schulz and Eugenia Ternovska},
  %series    = {EPiC Series},
  %volume    = {2},
  pages     = {1-11},
  year      = {2012}
  %publisher = {EasyChair}
}

@inproceedings{DBLP:conf/crypto/BartheGHB11,
  author    = {Gilles Barthe and
               Benjamin Gr{\'e}goire and
               Sylvain Heraud and
               Santiago Zanella B{\'e}guelin},
  title     = {Computer-Aided Security Proofs for the Working Cryptographer},
  booktitle = {CRYPTO},
  year      = {2011},
  pages     = {71-90}
}

@misc{our-devel,
  author = "Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel",
  title = "Formal development associated with this paper",
  howpublished = "\url{http://www21.in.tum.de/~traytel/codata_wit_devel.tar.gz}"
}

@misc{my-work-datatypes,
  author = "Andrei Popescu",
  title = "My Work on Datatypes",
  howpublished = "\url{http://www21.in.tum.de/~popescua/Work_on_Datatypes.pdf}"
}

@phdthesis{goedel-1929,
  author = {Kurt G{\"o}del},
  title = {\"Uber die Vollst\"andigkeit des Logikkalk\"uls},
  school = {Universit\"at Wien},
  type = "{Ph.D.}\ thesis",
  year = 1929}

@phdthesis{ilik-thesis,
  author = {Danko Ilik},
  title = {Constructive Completeness Proofs and Delimited Control},
  school = {\'Ecole Polytechnique},
  type = "{Ph.D.}\ thesis",
  year = 2010}


@phdthesis{haftmann-thesis,
  author = "Florian Haftmann",
  title = "Code Generation from Specifications in Higher-Order Logic",
  school = {Technische Universit\"at M\"unchen},
  year = 2009,
  type = "{Ph.D.}\ thesis"}

@inproceedings{haftmann-nipkow-2010,
  author    = {Florian Haftmann and Tobias Nipkow},
  title     = {Code Generation via Higher-Order Rewrite Systems},
  booktitle = {FLOPS 2010},
  year      = {2010},
  pages     = {103--117},
  publisher = {Springer}
}

@inproceedings{blanchette-et-al-2013-types,
  author = {Jasmin Christian Blanchette and Sascha B\"ohme and Andrei Popescu and Nicholas Smallbone},
  title = "Encoding Monomorphic and Polymorphic Types",
  booktitle = "TACAS",
  pages     = {493--507},
  year = 2013
}

@inproceedings{blanchette-frocos2013,
  author    = {Jasmin Christian Blanchette and
               Andrei Popescu},
  title     = {Mechanizing the Metatheory of {S}ledgehammer},
  booktitle = {FroCoS},
  year      = {2013},
  pages     = {245-260}
}




