I have now moved to London, as a senior lecturer at the Middlesex University. Of course, I will continue working with, and on, Isabelle.

Andrei Popescu


Graduate students I have advised
  1. Sudeep Kanav (coadvised jointly with Peter Lammich) A secure web interface for a verified conference management system (CoCon) Individual research project, Technische Universität München 2013

  2. Dmitriy Traytel (coadvised jointly with Jasmin Christian Blanchette) A category theory based (co)datatype package for Isabelle/HOL Master thesis, Technische Universität München 2012

  3. Andreas Schropp Instantiating deeply embedded many-sorted theories into HOL types in Isabelle Master thesis, Technische Universität München 2012

Our joint work on the topics of these theses and projects has yielded several publications: CAV 2014, IJCAR 2014, ITP 2014, CPP 2013, LICS 2012.


Complete list of publications (many also on DBLP)


On formal methods
  1. Draft Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel Foundational Extensible Corecursion Draft

  2. Draft Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel Witnessing (Co)datatypes Draft

  3. Draft Slides Sudeep Kanav, Peter Lammich, Andrei Popescu A Conference Management System with Verified Document Confidentiality CAV 2014
    LNCS 8559, 167-183, Springer

  4. Draft Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, Dmitriy Traytel Truly Modular (Co)datatypes for Isabelle/HOL ITP 2014
    LNCS 8558, 93-110, Springer

  5. Draft Slides Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel Cardinals in Isabelle/HOL ITP 2014
    LNCS 8558, 111-127, Springer

  6. Draft Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel Unified Classical Logic Completeness: A Coinductive Pearl IJCAR 2014
    LNCS 8562, 46-60, Springer

  7. Draft Slides Andreas Schropp, Andrei Popescu Nonfree Datatypes in Isabelle/HOL: Animating a Many-Sorted Metatheory CPP 2013
    LNCS 8307, 114-130, Springer

  8. Draft Slides Andrei Popescu, Johannes Hölzl, Tobias Nipkow Formalizing Probabilistic Noninterference CPP 2013
    LNCS 8307, 259-275, Springer

  9. Draft Andrei Popescu, Johannes Hölzl, Tobias Nipkow Formal Verification of Language-Based Concurrent Noninterference Journal of Formalized Reasoning 6(1), 2013

  10. Preprint Slides Jasmin Christian Blanchette, Andrei Popescu Mechanizing the metatheory of Sledgehammer FroCoS 2013
    LNCS 8152, 245-260, Springer

  11. Preprint Slides Andrei Popescu, Johannes Hölzl, Tobias Nipkow Noninterfering Schedulers: When Possibilistic Noninterference Implies Probabilistic Noninterference CALCO 2013
    LNCS 8089, 236-252, Springer

  12. Preprint Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone Encoding Monomorphic and Polymorphic Types TACAS 2013
    LNCS 7795, 493-507, Springer

  13. Preprint Andrei Popescu, Johannes Hölzl, Tobias Nipkow Proving Concurrent Noninterference CPP 2012
    LNCS 7795, 109-125, Springer
    Proud receiver of the RS3 best paper award for 2012-2013

  14. Preprint Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification ITP 2012
    LNCS 7406, 345-360, Springer

  15. Preprint Slides Dmitriy Traytel, Andrei Popescu, Jasmin Christian Blanchette Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving LICS 2012
    596-605, IEEE

  16. Preprint Andrei Popescu, Elsa L. Gunter Recursion principles for syntax with bindings and substitution ICFP 2011
    346-358, ACM

  17. Preprint Slides Slides Andrei Popescu, Elsa L. Gunter, Christopher J. Osborn Strong Normalization for System F by HOAS on Top of FOAS LICS 2010
    31-40, IEEE

  18. Preprint Slides Andrei Popescu, Elsa L. Gunter Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization FOSSACS 2010
    LNCS 6014, 109-127, Springer

  19. Preprint Andrei Popescu, Traian-Florin Serbanuta, Grigore Rosu A semantic approach to interpolation Theoretical Computer Science 410(12-13): 1109-1128 (2009)

  20. Preprint Slides Andrei Popescu Weak Bisimilarity Coalgebraically CALCO 2009
    LNCS 5728, 157-172, Springer

  21. Elsa L. Gunter, Christopher J. Osborn, Andrei Popescu Theory support for weak higher order abstract syntax in Isabelle/HOL LMFTP 2009
    12-20, ACM

  22. Preprint Andrei Popescu, Grigore Rosu Term-Generic Logic. WADT 2008
    LNCS 5486, 290-307, Springer

  23. Daniel Gaina, Andrei Popescu An Institution-Independent Proof of the Robinson Consistency Theorem Studia Logica 85(1): 41-73 (2007)

  24. Daniel Gaina, Andrei Popescu An Institution-independent Generalization of Tarski's Elementary Chain Theorem Journal of Logic and Computation 16(6): 713-735 (2006)

  25. Andrei Popescu, Traian Serbanuta, Grigore Rosu A Semantic Approach to Interpolation FOSSACS 2006
    LNCS 3921, 307-321, Springer

  26. Preprint Andrei Popescu, Grigore Rosu Behavioral Extensions of Institutions CALCO 2005
    LNCS 3629, 331-347, Springer

  27. Andrei Popescu Languages Generated Using an Abstract Catenation Grammars 7: 31-40 (2004)

Ph.D. thesis
  1. Preprint   Contributions to the Theory of Syntax with Bindings and to Process Algebra University of Illinois at Urbana-Champaign (2010)
    Advisor: Elsa Gunter

Isabelle Developments in The Archive of Formal Proofs
  1. Andrei Popescu, Peter Lammich Bounded-Deducibility Security Archive of Formal Proofs (2014)

  2. Markus N. Rabe, Peter Lammich, Andrei Popescu A shallow embedding of HyperCTL* Archive of Formal Proofs (2014)

  3. Andrei Popescu, Johannes Hölzl Probabilistic Noninterference Archive of Formal Proofs (2014)

  4. Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel Abstract Completeness Archive of Formal Proofs (2014)

  5. Jasmin Christian Blanchette, Andrei Popescu Sound and Complete Sort Encodings for First-Order Logic Archive of Formal Proofs (2013)

  6. Andrei Popescu, Johannes Hölzl Possibilistic Noninterference Archive of Formal Proofs (2012)

  7. Andrei Popescu Ordinals and Cardinals Archive of Formal Proofs (2009)

On fuzzy logic and algebra
  1. Andrei Popescu Some algebraic theory for many-valued relation algebras Algebra Universalis 56: 211-235 (2007)

  2. George Georgescu, Andrei Popescu A common generalization for MV-algebras and Lukasiewicz-Moisil algebras Archive for Mathematical Logic 45(8): 947-981 (2006)

  3. George Georgescu, Ioana Leustean, Andrei Popescu Order convergence and distance on Lukasiewicz-Moisil algebras Journal of Multiple-Valued Logic and Soft Computing 12(1-2): 33-69 (2006)

  4. George Georgescu, Andrei Popescu A new class of probabilities on Lukasiewicz-Moisil algebras Journal of Multiple-Valued Logic and Soft Computing 12(3-4): 337-354 (2006)

  5. George Georgescu, Andrei Popescu Similarity Convergence in Residuated Structures Logic Journal of the IGPL 13(4): 389-413 (2005)

  6. Andrei Popescu Lukasiewicz-Moisil Relation Algebras Studia Logica 81(2): 167-189 (2005)

  7. Andrei Popescu Many-Valued Relation Algebras Algebra Universalis 53: 73-108 (2005)

  8. George Georgescu, Andrei Popescu Non-dual fuzzy connections Archive for Mathematical Logic 43(8): 1009-1039 (2004)

  9. George Georgescu, Andrei Popescu Non-commutative fuzzy structures and pairs of weak negations Fuzzy Sets and Systems 143(1): 129-155 (2004)

  10. Andrei Popescu A general approach to fuzzy concepts Mathematical Logic Quarterly 50(3): 265-280 (2004)

  11. George Georgescu, Andrei Popescu Non-commutative fuzzy Galois connections Soft Computing 7(7): 458-467 (2003)

  12. George Georgescu, Andrei Popescu Concept lattices and similarity in non-commutative fuzzy logic Fundamenta Informaticae 53(1): 23-54 (2002)