@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},
}
@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{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-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}"}
@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}
}
@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}
}
@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{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}
}
@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{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\tthttp://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\tthttp://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 Reportnumber 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, Volume25"}
@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, pages391--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, Volume16, Number7, pages24--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 {\emJournal 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}
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, pages30--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"}
@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"
}
@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}
}
@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.
{\tthttp://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"}
@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. {\tthttp://issan.informatik.uni-dortmund.de/~peter}"}
@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 incoinductiveproof},
booktitle = {POPL},
year = {2013},
pages = {193-206}
}
@article{plotkin-CBNandCBVandLambda,
author = {Gordon D. Plotkin},
title = {Call-by-Name, Call-by-Valueand 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"}
@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= "{\tthttp://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\tthttp://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"}
@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 andinduction},
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"}
%%% TODO: Complete
@inproceedings{AbelA99,
author = {Andreas Abel and
Thorsten Altenkirch},
title = {A Predicative Strong Normalisation Prooffor a lambda-Calculus with Interleaving InductiveTypes},
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}
}
@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"}
@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 TheoremProver}, 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"}
@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)"}
@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 Notesin Mathematics}, number = {454}, year = {1975}}
@article{mak-fir, author = {Michael Makkai and G. E. Reyes}, title = {First Order Categorical Logic},
journal = {Lecture Notesin 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 SyntaxwithInductionin 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{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 Structurefor Higher Order Quotients},
booktitle = {TPHOLs 2005},
pages = {130--146},
editor = {Joe Hurd and
Thomas F. Melham},
publisher = {Springer},
series = {LNCS},
volume = {3603},
year = {2005}
}
@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 Theoremfor {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 Theoremand Bar Induction---{W}alking
through Infinite Trees with Mixed Inductionand 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{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 toTheorem 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}"
}
@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)inductiveand (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 Theoremfor 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"}
@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}"
}
@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}
}
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.244 Sekunden
(vorverarbeitet am 2026-06-10)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
