Andrei Popescu

I am a researcher at the Informatics Institute, Technical University Munich, at the Chair for Logic and Verification headed by Tobias Nipkow and patroned by goddess Isabelle. My main research interests are in Mathematical Logic, Type Systems, Process Algebra, Category Theory and Theorem Proving, and intersections of these areas. My recent work focuses on (co)recursion and (co)induction principles for various data types, including syntax with bindings, and their representation in Isabelle/HOL. In particular, I have (co)designed a new (co)datatype package for Isabelle/HOL. I am also interested in information-flow security, and am involved in the RS3 project Security Type Systems and Deduction. In the past, I have worked on Fuzzy Logic and Abstract Model Theory.

Address: Institut für Informatik, Technische Universität München, Boltzmannstr. 3, 85748 Garching, Germany
Email: uuomul the at sign yahoo.com


Full list of publications (see also DBLP)

On formal methods

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

  2. Preprint Andrei Popescu, Johannes Hölzl, Tobias Nipkow Proving Concurrent Noninterference. CPP 2012: 109-125

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

  4. Preprint 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

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

  6. Preprint Andrei Popescu, Elsa L. Gunter Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization. FOSSACS 2010: 109-127

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

  8. Preprint Andrei Popescu, Traian-Florin Serbanuta, Grigore Rosu A semantic approach to interpolation. Theor. Comput. Sci. 410(12-13): 1109-1128 (2009)

  9. Preprint Andrei Popescu Weak Bisimilarity Coalgebraically. CALCO 2009: 157-172

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

  11. Preprint Andrei Popescu, Grigore Rosu Term-Generic Logic. WADT 2008: 290-307

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

  13. Preprint Daniel Gaina, Andrei Popescu An Institution-independent Generalization of Tarski's Elementary Chain Theorem. J. Log. Comput. 16(6): 713-735 (2006)

  14. Preprint Andrei Popescu, Traian Serbanuta, Grigore Rosu A Semantic Approach to Interpolation. FoSSaCS 2006: 307-321

  15. Preprint Andrei Popescu, Grigore Rosu Behavioral Extensions of Institutions. CALCO 2005: 331-347

  16. Preprint 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

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

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

On fuzzy logic and algebra

  1. Preprint Andrei Popescu Some algebraic theory for many-valued relation algebras. Algebra Universalis 56: 211-235 (2007)

  2. Preprint George Georgescu, Andrei Popescu A common generalization for MV-algebras and Lukasiewicz-Moisil algebras. Arch. Math. Log. 45(8): 947-981 (2006)

  3. Preprint 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. Preprint 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. Preprint George Georgescu, Andrei Popescu Similarity Convergence in Residuated Structures. Logic Journal of the IGPL 13(4): 389-413 (2005)

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

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

  8. Preprint George Georgescu, Andrei Popescu Non-dual fuzzy connections. Arch. Math. Log. 43(8): 1009-1039 (2004)

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

  10. Preprint Andrei Popescu A general approach to fuzzy concepts. Math. Log. Q. 50(3): 265-280 (2004)

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

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

Ph.D. thesis

  1. Preprint  Many-Valued Relation Algebra University of Bucharest (2005)
    Advisor: George Georgescu