Professor

Andrei

Popescu

Journal articles

• Derrick J, Dongol B, Edmonds C, Griffin M, Popescu A & Wright J (2025) Relative Security: (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities in Isabelle/HOL. Journal of Automated Reasoning, 69(4).
• Cohen L, Jabarin A, Popescu A & Rowe RNS (2024) The complex(ity) landscape of checking infinite descent. Proceedings of the ACM on Programming Languages, 8(POPL), 1352-1384. View this article in WRRO
• Popescu A (2024) Nominal recursors as epi-recursors. Proceedings of the ACM on Programming Languages, 8(POPL). View this article in WRRO
• Popescu A (2023) Rensets and renaming-based recursion for syntax with bindings extended version. Journal of Automated Reasoning, 67(3). View this article in WRRO
• Popescu A & Traytel D (2023) Admissible types-to-PERs relativization in higher-order logic. Proceedings of the ACM on Programming Languages, 7(POPL), 1214-1245. View this article in WRRO
• Popescu A & Traytel D (2021) Distilling the requirements of Gödel’s incompleteness theorems with a proof assistant. Journal of Automated Reasoning, 65(7), 1027-1070.
• Popescu A, Lammich P & Hou P (2021) CoCon: a conference management system with formally verified document confidentiality. Journal of Automated Reasoning, 65(2), 321-356. View this article in WRRO
• (2020) Preface. IOP Conference Series: Materials Science and Engineering, 997(1), 011001-011001.
• Gheri L & Popescu A (2020) A formalized general theory of syntax with bindings: extended version. Journal of Automated Reasoning, 64(4), 641-675.
• Blanchette JC, Gheri L, Popescu A & Traytel D (2019) Bindings as bounded natural functors. Proceedings of the ACM on Programming Languages, 3(POPL), ---.
• Cerrito S & Popescu A (2019) Preface. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 11714 LNAI, V-vi.
• Herzig A & Popescu A (2019) Preface. Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 11715 LNAI, v-vi.
• Kunčar O & Popescu A (2019) From types to sets by local type definition in higher-order logic. Journal of Automated Reasoning, 62(2), 237-260.
• Kunčar O & Popescu A (2019) A consistent foundation for Isabelle/HOL. Journal of Automated Reasoning, 62(4), 531-555.
• Avigad J, Blanchette JC, Klein G, Paulson L, Popescu A & Snelting G (2018) Introduction to milestones in interactive theorem proving. Journal of Automated Reasoning, 61(1-4), 1-8. View this article in WRRO
• Kunčar O & Popescu A (2018) Safety and conservativity of definitions in HOL and Isabelle/HOL. Proceedings of the ACM on Programming Languages, 2(POPL), ---.
• Bauereiß T, Pesenti Gritti A, Popescu A & Raimondi F (2018) CoSMed: a confidentiality-verified social media platform. Journal of Automated Reasoning, 61(1-4), 113-139.
• Blanchette J, Böhme S, Popescu A & Smallbone N (2017) Encoding monomorphic and polymorphic types. Logical Methods in Computer Science, 12(4), 1-52.
• Blanchette JC, Popescu A & Traytel D (2017) Soundness and completeness proofs by coinductive methods. Journal of Automated Reasoning, 58(1), 149-179.
• (2016) 7th International Conference on Advanced Concepts in Mechanical Engineering. IOP Conference Series: Materials Science and Engineering, 147, 011001-011001.
• Blanchette JC, Popescu A & Traytel D (2015) Foundational extensible corecursion: a proof assistant perspective. ACM SIGPLAN Notices, 50(9), 192-204. View this article in WRRO
• Blanchette JC, Popescu A & Traytel D (2015) Witnessing (Co)datatypes. Programming Languages and Systems: 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings, 9032, 359-382. View this article in WRRO
• Popescu A & Roşu G (2015) Term-generic logic. Theoretical Computer Science, 577, 1-24. View this article in WRRO
• Nipkow T & Popescu A (2014) Making security type systems less ad hoc. IT - Information Technology, 56(6), 267-272. View this article in WRRO
• Doroftei I, Oprisan C & Popescu A (2014) Preface. Applied Mechanics and Materials, 659.
• Doroftei I, Oprisan C & Popescu A (2014) Preface. Applied Mechanics and Materials, 658.
• Popescu A, Hölzl J & Nipkow T (2013) Formal verification of language-based concurrent noninterference. Journal of Formalized Reasoning, 6(1), 1-30.
• Popescu A & Gunter EL (2011) Recursion principles for syntax with bindings and substitution. ACM SIGPLAN Notices, 46(9), 346-358.
• Popescu A, Şerbănuţă TF & Roşu G (2009) A semantic approach to interpolation. Theoretical Computer Science, 410(12-13), 1109-1128.
• Popescu A (2007) Some algebraic theory for many-valued relation algebras. Algebra universalis, 56(2), 211-235.
• Gâinâ D & Popescu A (2007) An Institution-Independent Proof of the Robinson Consistency Theorem. Studia Logica, 85(1), 41-73.
• Georgescu G & Popescu A (2006) A new class of probabilities on Łukasiewicz-Moisil algebras. Journal of Multiple Valued Logic and Soft Computing, 12(3-4 SPEC. ISS.), 337-354.
• Georgescu G & Popescu A (2006) A common generalization for MV-algebras and Łukasiewicz–Moisil algebras. Archive for Mathematical Logic, 45(8), 947-981.
• Georgescu G, Leuştean I & Popescu A (2006) Order convergence and distance on Łukasiewicz-Moisil algebras. Journal of Multiple Valued Logic and Soft Computing, 12(1-2), 33-69.
• Popescu A (2005) Łukasiewicz-Moisil Relation Algebras. Studia Logica, 81(2), 167-189.
• Popescu A (2005) Many-valued relation algebras. Algebra universalis, 53(1), 73-108.
• Georgescu G & Popescu A (2004) Non-dual fuzzy connections. Archive for Mathematical Logic, 43(8), 1009-1039.
• Popescu A (2004) A general approach to fuzzy concepts. Mathematical Logic Quarterly, 50(3), 265-280.
• Georgescu G & Popescu A (2004) Non-commutative fuzzy structures and pairs of weak negations. Fuzzy Sets and Systems, 143(1), 129-155.
• Georgescu G & Popescu A (2003) Non-commutative fuzzy Galois connections. Soft Computing, 7(7), 458-467.
• Georgescu G & Popescu A (2002) Concept lattices and similarity in non-commutative fuzzy logic. Fundamenta Informaticae, 53(1), 23-54.
• Tomas E, Popescu A, Zuivertz A, Jucu V, Czabor F & Cristescu C (1995) Study of the antiviral activity of some new classes of AS-triazine derivatives (preliminary note).. Rom J Virol, 46(1-2), 51-56.
• Zaharia CN, Cristea M, Petrescu A, Jucu V & Popescu AI (1994) Investigations on the influence of the experimental infection with the herpes simplex virus type 1 on the electrophoretic mobility of some cultured cells.. Rev Roum Virol, 45(1-2), 55-67.
• Popescu A & Cernescu C (1994) CD 26--to be or not to be a cofactor for CD 4 receptor of human immunodeficiency viruses.. Rev Roum Virol, 45(3-4), 203-209.
• Popescu A, Zuivertz A, Olinescu R, Tomas S, Tomas E & Jucu V (1992) Antiviral activity of some copper complexes of symmetrical triazines.. Rev Roum Virol, 43(3-4), 181-184.
• Olinescu R, Săvoiu D, Popescu A, Zuivertz A & Tomas E (1992) Induction of chemiluminescent emission in polymorphonuclear leucocytes stimulated by Sendai virus.. Rev Roum Virol, 43(3-4), 175-179.
• Popescu A, Jucu V, Tomas E, Zuiwertz A, Cristescu C & Tomas S (1992) Antiviral activity of some copper complexes of as-triazines.. Rev Roum Virol, 43(1-2), 125-126.
• Tomas ST, Titire A, Popescu A, Tomas E & Cajal N (1991) Potential antiviral activity of copper complexes, derived from symmetrical triazines hydrazones.. Rev Roum Virol, 42(1-2), 71-75.
• Tomas E, Popescu A, Titire A, Cajal N, Cristescu C & Tomas S (1989) Viral infection correlated with superoxide anion radicals production and natural and synthetic copper complexes.. Virologie, 40(4), 305-312.
• Zuivertz A, Tomas S, Popescu A, Cristescu C & Tomas E (1988) Effects of asymmetrical triazine copper complexes on superoxide radical formation and on the Sendai virus multiplication.. Virologie, 39(3), 217-220.
• Tomas E, Dumitrescu SM, Popescu A & Cajal N (1985) Structural particularities of parainfluenza type 1 (Sendai) virus progens obtained by cultivation in the presence of ceruloplasmin.. Virologie, 36(3), 201-206.
• Tomas E, Samuel I, Popescu A & Cajal N (1983) Comparative study of some characteristics of influenza virus A/PR8/34 (H1N1) cultivated on chorioallantoic membrane fragments in the presence of ceruloplasmin or of parainfluenza type I (Sendai) virus.. Virologie, 34(4), 295-301.
• Petrescu A, Cajal N, Broniţki A, Mihail A, Teodosiu O, Popescu G, Isaia G & Popescu A (1977) The experience of the "Stefan S. Nicolau" Institue of Virology in the preparation of administration of inactivated influenza vaccines applicable by nasal or oral route.. Virologie, 28(3), 213-217.
• Potop I, Boeru V, Prahoveanu E, Simionescu L, Petrescu A & Popescu A (1977) Stimulation of anti-influenza serum antibody formation in the rat using bovine thymus polypeptide extract.. Endocrinologie, 15(1), 13-18.
• Sahnazarov N, Mutiu A, Dumitrescu SM, Cajal N, Popescu A & Constantinescu O (1977) Cellular transformation in vitro induced by herpes simplex virus (HSV). Note IV. Presence of viral antigens and herpes-like particles in the T-TR1 tumor cell line.. Virologie, 28(4), 283-287.
• Petrescu A, Broniţki AL, Teodosiu O, Mihail A, Popescu A, Cojiţă M, Petrişor L, Ialomiţeanu M, Mîşcă C, Sferdean O , Botgros V et al (1976) Virological study of some influenza outbreaks in the period January--March 1975.. Virologie, 27(2), 111-114.
• Petrescu A, Mihail A, Popescu A, Cojiţă M, Sternberg I, Steiner N & Hondor C (1976) Bivalent influenza vaccination with inactivated vaccines administered by nasal or oral route.. Virologie, 27(1), 41-45.
• Petrescu A, Broniţki A, Mihal A, Teodosiu O, Isaia G, Popescu A, Doicescu M, Diaconu A, Oroian E, Bolgar E , Varga N et al (1975) [Studies of the influenza epidemic of January-March, 1974].. Rev Ig Bacteriol Virusol Parazitol Epidemiol Pneumoftiziol Bacteriol Virusol Parazitol Epidemiol, 20(3), 147-152.
• Teodosiu O, Sărăţeanu D, Popescu A & Mihail A (1974) Study of some influenza virus strains isolated in Romania during the epidemics of 1971-1972.. Rev Roum Virol (1972), 11(2), 171-177.
• Bronitki A, Sărăţeanu D, Surdan C & Popescu A (1974) Equine epizootic caused by influenza virus type A2/England 42/72.. Rev Roum Virol (1972), 25(3), 207-210.
• Sărăţeanu D, Broniţki A, Popescu A, Teodosiu O & Isaia G (1974) Incidence of coronavirus OC43 antibodies among the population of Romania.. Rev Roum Virol (1972), 25(3), 255-258.
• Cajal N, Sărăteanu D, Petrescu A, Mihail A, Popescu A & Teodosiu O (1974) Preliminary data on the efficiency of an inactivated influenza vaccine administered by oral route.. Rev Roum Virol (1972), 25(1), 23-27.
• Cajal N, Sărăţeanu D, Petrescu A, Mihail A, Popescu A & Teodosiu O (1973) [Study of the effectiveness of an inactivated influenza vaccine in intra nasal administration. II. Observations made during the epidemic of December 1972].. Stud Cercet Virusol, 24(5), 357-362.
• Moisa I, Broniţki A, Popescu A & Marinescu G (1970) [Studies of influenza virus infections in the population of the city of Bucharest in the period of June 1969--April 1970].. Stud Cercet Inframicrobiol, 21(6), 475-489.
• Moisa I, Popescu A, Broniţki A & Marinescu G (1970) [Laboratory studies of the epidemic of influenza in Bucharest (April-May 1969)].. Stud Cercet Inframicrobiol, 21(1), 7-23.
• Măgureanu E, Grobnicu M, Muşetescu M, Dumitrescu S & Popescu A (1969) [Study of anti-rubella immunity in the Socialist Republic of Rumania with the hemagglutination inhibition (HAI) test].. Microbiol Parazitol Epidemiol (Bucur), 14(3), 215-220.
• Moisa I, Broniţki A, Popescu A, Marinescu G & Malian A (1969) [Laboratory study of several epidemic foci of influenza during the years 1967 and 1968].. Stud Cercet Inframicrobiol, 20(2), 99-108.
• Cepleanu M, Sorodoc Y, Băhnăreanu D, Bîrzu N, Doicescu M, Ianopol L, Ionescu N, Popescu A, Olaru G, Tîrnoveanu G , Totescu E et al (1967) [Incidence of anti-measles hemagglutination-inhibiting antibodies in some regions of the Rumanian Socialist Republic].. Stud Cercet Inframicrobiol, 18(1), 45-54.
• Broniţki A, Barbu C, Popescu A, Moisa I & Malian A (1966) [Laboratory research on the influenza epidemic of January-February 1966 in Bucharest].. Stud Cercet Inframicrobiol, 17(5), 367-370.
• Popescu A () Supernominal Datatypes and Codatatypes. Electronic Proceedings in Theoretical Computer Science, 332.
• () The 8th International Conference on Advanced Concepts in Mechanical Engineering. IOP Conference Series: Materials Science and Engineering, 444, 011001-011001.
• () An Institution-independent Generalization of Tarski's Elementary Chain Theorem. Journal of Logic and Computation, 17(3), 605-605.
• Gaina D & Popescu A () An Institution-independent Generalization of Tarski's Elementary Chain Theorem. Journal of Logic and Computation, 16(6), 713-735.

Book chapters

• Derrick J, Edmonds C, Popescu A & Wright J (2026) Rely-Guarantee Is Coinductive In Krebbers R (Ed.), Lecture Notes in Computer Science (pp. 220-251). Springer Nature Switzerland
• Graczyk A, Hadjikosti M & Popescu A (2024) A Framework for Verifying the Collision Freeness of Collaborative Robots (Work in Progress), Lecture Notes in Computer Science (pp. 391-397). Springer Nature Switzerland
• Popescu A & Roşu G (2009) Term-Generic Logic, Lecture Notes in Computer Science (pp. 290-307). Springer Berlin Heidelberg
• Popescu A, Şerbănuţă TF & Roşu G (2006) A Semantic Approach to Interpolation, Lecture Notes in Computer Science (pp. 307-321). Springer Berlin Heidelberg
• Popescu A & Roşu G (2005) Behavioral Extensions of Institutions, Lecture Notes in Computer Science (pp. 331-347). Springer Berlin Heidelberg

Conference proceedings

• Wright J, Cohen L, Rowe RNS & Popescu A (2026) Certified Infinite Descent Criteria in Isabelle/HOL. Leibniz International Proceedings in Informatics Lipics, Vol. 382
• van Brügge J, Popescu A & Traytel D (2025) Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL. Leibniz International Proceedings in Informatics Lipics, Vol. 352
• Popescu A (2025) Completing Gordon’s Higher-Order Logic. 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vol. 00 (pp 1-15)
• van Brügge J, McKinna J, Popescu A & Traytel D (2025) Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings. Proceedings of the ACM on Programming Languages, Vol. 9(POPL) (pp 1687-1718)
• Dongol B, Griffin M, Popescu A & Wright J (2024) Relative security: formally modeling and (dis)proving resilience against semantic optimization vulnerabilities. 2024 IEEE 37th Computer Security Foundations Symposium (CSF) (pp 403-418). Enschede, Netherlands, 8 July 2024 - 8 July 2024. View this article in WRRO
• Buday G & Popescu A (2024) Isomorphic Transfer Infrastructure for Nested Types in Isabelle/HOL (Work in Progress). Ceur Workshop Proceedings, Vol. 3860 (pp 38-48)
• Popescu A (2022) Rensets and renaming-based recursion for syntax with bindings. Automated Reasoning: 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022, Proceedings (pp 618-639). Haifa, Israel, 8 August 2022 - 10 August 2022.
• Popescu A, Bauereiss T & Lammich P (2021) Bounded-deducibility security. 12th International Conference on Interactive Theorem Proving (ITP 2021), Vol. 193 (pp 3:1-3:20). Online, 29 June 2021 - 1 July 2021.
• (2020) FroCoS/TABLEAUX 2019 COSPONSORED BY THE ASSOCIATION FOR SYMBOLIC LOGIC London, UK September 2–6, 2019. The Bulletin of Symbolic Logic, Vol. 26(3-4) (pp 312-312)
• Popescu A & Traytel D (2019) A formally verified abstract account of Gödel’s incompleteness theorems. Automated Deduction – CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings, Vol. LNAI 11716 (pp 442-461). Natal, Brazil, 27 August 2019 - 30 August 2019.
• Biendarra J, Blanchette JC, Bouzy A, Desharnais M, Fleury M, Hölzl J, Kunčar O, Lochbihler A, Meier F, Panny L , Popescu A et al (2017) Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic (pp 3-21)
• Gheri L & Popescu A (2017) A formalized general theory of syntax with bindings. Interactive Theorem Proving: 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings, Vol. 10499 (pp 241-261). Brasília, Brazil, 26 September 2017 - 29 September 2017.
• Blanchette JC, Meier F, Popescu A & Traytel D (2017) Foundational nonuniform (Co)datatypes for higher-order logic. 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Reykjavik, Iceland, 20 June 2017 - 23 June 2017.
• Bauereiß T, Gritti AP, Popescu A & Raimondi F (2017) CoSMeDis : a distributed social media platform with formally verified confidentiality guarantees. 2017 IEEE Symposium on Security and Privacy (SP) (pp 729-748). San Jose, CA, USA, 22 May 2017 - 26 May 2017.
• Blanchette JC, Bouzy A, Lochbihler A, Popescu A & Traytel D (2017) Friends with benefits: implementing corecursion in foundational proof assistants. Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings, Vol. LNTCS,volume 10201 (pp 111-140). Uppsala, Sweden, 22 April 2017 - 29 April 2017.
• Kunčar O & Popescu A (2017) Comprehending Isabelle/HOL’s Consistency. Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings, Vol. LNTCS,volume 10201 (pp 724-749). Uppsala, Sweden, 22 April 2017 - 29 April 2017.
• Bauereiß T, Pesenti Gritti A, Popescu A & Raimondi F (2016) CoSMed: a confidentiality-verified social media platform. Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings, Vol. LNTCS,volume 9807 (pp 87-106). Nancy, France, 22 August 2016 - 25 August 2016.
• Kunčar O & Popescu A (2016) From types to sets by local type definitions in higher-order logic. Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings, Vol. LNTCS,volume 9807 (pp 200-218). Nancy, France, 22 August 2016 - 25 August 2016.
• Kunčar O & Popescu A (2015) A Consistent Foundation for Isabelle/HOL (pp 234-252)
• Blanchette JC, Popescu A & Traytel D (2015) Foundational extensible corecursion : a proof assistant perspective. ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (pp 192-204). Vancouver, BC, Canada, 31 August 2015 - 31 August 2015. View this article in WRRO
• Blanchette JC, Popescu A & Traytel D (2014) Unified Classical Logic Completeness (pp 46-60)
• Kanav S, Lammich P & Popescu A (2014) A Conference Management System with Verified Document Confidentiality (pp 167-183)
• Blanchette JC, Popescu A & Traytel D (2014) Cardinals in Isabelle/HOL (pp 111-127)
• Blanchette JC, Hölzl J, Lochbihler A, Panny L, Popescu A & Traytel D (2014) Truly Modular (Co)datatypes for Isabelle/HOL (pp 93-110)
• Popescu A, Hölzl J & Nipkow T (2013) Formalizing Probabilistic Noninterference (pp 259-275)
• Blanchette JC & Popescu A (2013) Mechanizing the Metatheory of Sledgehammer (pp 245-260)
• Schropp A & Popescu A (2013) Nonfree Datatypes in Isabelle/HOL (pp 114-130)
• Popescu A, Hölzl J & Nipkow T (2013) Noninterfering Schedulers (pp 236-252)
• Blanchette JC, Böhme S, Popescu A & Smallbone N (2013) Encoding Monomorphic and Polymorphic Types (pp 493-507)
• Popescu A, Hölzl J & Nipkow T (2012) Proving Concurrent Noninterference (pp 109-125)
• Traytel D, Popescu A & Blanchette JC (2012) Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. 2012 27th Annual IEEE Symposium on Logic in Computer Science (pp 596-605), 25 June 2012 - 28 June 2012.
• Blanchette JC, Popescu A, Wand D & Weidenbach C (2012) More SPASS with Isabelle (pp 345-360)
• Popescu A & Gunter EL (2011) Recursion principles for syntax with bindings and substitution. Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (pp 346-358)
• Popescu A & Gunter EL (2010) Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization (pp 109-127)
• Popescu A, Gunter EL & Osborn CJ (2010) Strong Normalization for System F by HOAS on Top of FOAS. 2010 25th Annual IEEE Symposium on Logic in Computer Science (pp 31-40), 11 July 2010 - 14 July 2010.
• Gunter EL, Osborn CJ & Popescu A (2009) Theory support for weak higher order abstract syntax in Isabelle/HOL. Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (pp 12-20)
• Popescu A (2009) Weak Bisimilarity Coalgebraically (pp 157-172)
• Georgescu G & Popescu A (2005) Similarity Convergence in Residuated Structures. Logic Journal of the IGPL, Vol. 13(4) (pp 389-413)

Preprints

• Kappelmann K, Schäffeler M, Stevens L, Abdulaziz M, Popescu A & Traytel D (2026) Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints, arXiv.
• Popescu A (2023) Rensets and Renaming-Based Recursion for Syntax with Bindings: Extended Version, Research Square Platform LLC.
• Popescu A (2023) Nominal Recursors as Epi-Recursors: Extended Technical Report, arXiv.
• Popescu A (2022) Rensets and Renaming-Based Recursion for Syntax with Bindings, arXiv.
• Gheri L & Popescu A (2021) Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS, arXiv.
• Gheri L & Popescu A (2017) A Formalized General Theory of Syntax with Bindings, arXiv.
• Blanchette JC, Böhme S, Popescu A & Smallbone N (2016) Encoding Monomorphic and Polymorphic Types, arXiv.
• Blanchette JC, Popescu A & Traytel D (2015) Foundational Extensible Corecursion, arXiv.