Professor Andrei Popescu

PhD

School of Computer Science

Professor of Computing Foundations

School Programmes Lead (PGT)

Member of the Security of Advanced Systems research group

Member of the Foundations of Computation research group

Profile photo of Andrei Popescu
Profile picture of Profile photo of Andrei Popescu
a.popescu@sheffield.ac.uk
Regent Court (CS)

Full contact details

Professor Andrei Popescu
School of Computer Science
Regent Court (CS)
211 Portobello
Sheffield
S1 4DP
Profile

Andrei became a Senior Lecturer in the Security of Advanced Systems group in May 2020, and was promoted to Professor of Computing Foundations in January 2026. Previously, he worked as a Lecturer at Middlesex University and as a postdoctoral researcher at TU Munich. He has a Ph.D. in computer science from the University of Illinois at Urbana-Champaign and a Ph.D. in mathematics from the University of Bucharest.

Research interests
  • Proof assistants
  • Information flow security
  • Inductive and coinductive datatypes
  • Automated deduction
  • Syntax with bindings
Publications

Journal articles

  • Derrick J, Dongol B, Edmonds C, Griffin M, Popescu A & Wright J (2025) . Journal of Automated Reasoning, 69(4).
  • Cohen L, Jabarin A, Popescu A & Rowe RNS (2024) . Proceedings of the ACM on Programming Languages, 8(POPL), 1352-1384.
  • Popescu A (2024) . Proceedings of the ACM on Programming Languages, 8(POPL).
  • Popescu A (2023) . Journal of Automated Reasoning, 67(3).
  • Popescu A & Traytel D (2023) . Proceedings of the ACM on Programming Languages, 7(POPL), 1214-1245.
  • Popescu A & Traytel D (2021) . Journal of Automated Reasoning, 65(7), 1027-1070.
  • Popescu A, Lammich P & Hou P (2021) . Journal of Automated Reasoning, 65(2), 321-356.
  • (2020) . IOP Conference Series: Materials Science and Engineering, 997(1), 011001-011001.
  • Gheri L & Popescu A (2020) . Journal of Automated Reasoning, 64(4), 641-675.
  • Blanchette JC, Gheri L, Popescu A & Traytel D (2019) . 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) . Journal of Automated Reasoning, 62(2), 237-260.
  • Kunčar O & Popescu A (2019) . Journal of Automated Reasoning, 62(4), 531-555.
  • Avigad J, Blanchette JC, Klein G, Paulson L, Popescu A & Snelting G (2018) . Journal of Automated Reasoning, 61(1-4), 1-8.
  • Kunčar O & Popescu A (2018) . Proceedings of the ACM on Programming Languages, 2(POPL), ---.
  • Bauereiß T, Pesenti Gritti A, Popescu A & Raimondi F (2018) . Journal of Automated Reasoning, 61(1-4), 113-139.
  • Blanchette J, Böhme S, Popescu A & Smallbone N (2017) . Logical Methods in Computer Science, 12(4), 1-52.
  • Blanchette JC, Popescu A & Traytel D (2017) . Journal of Automated Reasoning, 58(1), 149-179.
  • (2016) . IOP Conference Series: Materials Science and Engineering, 147, 011001-011001.
  • Blanchette JC, Popescu A & Traytel D (2015) . ACM SIGPLAN Notices, 50(9), 192-204.
  • Blanchette JC, Popescu A & Traytel D (2015) . 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.
  • Popescu A & Roşu G (2015) . Theoretical Computer Science, 577, 1-24.
  • Nipkow T & Popescu A (2014) . IT - Information Technology, 56(6), 267-272.
  • 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) . ACM SIGPLAN Notices, 46(9), 346-358.
  • Popescu A, Şerbănuţă TF & Roşu G (2009) . Theoretical Computer Science, 410(12-13), 1109-1128.
  • Popescu A (2007) . Algebra universalis, 56(2), 211-235.
  • Gâinâ D & Popescu A (2007) . 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) . 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) . Studia Logica, 81(2), 167-189.
  • Popescu A (2005) . Algebra universalis, 53(1), 73-108.
  • Georgescu G & Popescu A (2004) . Archive for Mathematical Logic, 43(8), 1009-1039.
  • Popescu A (2004) . Mathematical Logic Quarterly, 50(3), 265-280.
  • Georgescu G & Popescu A (2004) . Fuzzy Sets and Systems, 143(1), 129-155.
  • Georgescu G & Popescu A (2003) . 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.
  • Popescu A () . Electronic Proceedings in Theoretical Computer Science, 332.
  • () . IOP Conference Series: Materials Science and Engineering, 444, 011001-011001.
  • () . Journal of Logic and Computation, 17(3), 605-605.
  • Gaina D & Popescu A () . Journal of Logic and Computation, 16(6), 713-735.

Book chapters

  • Derrick J, Edmonds C, Popescu A & Wright J (2026) In Krebbers R (Ed.), Lecture Notes in Computer Science (pp. 220-251). Springer Nature Switzerland
  • Graczyk A, Hadjikosti M & Popescu A (2024) , Lecture Notes in Computer Science (pp. 391-397). Springer Nature Switzerland
  • Popescu A & Roşu G (2009) , Lecture Notes in Computer Science (pp. 290-307). Springer Berlin Heidelberg
  • Popescu A, Şerbănuţă TF & Roşu G (2006) , Lecture Notes in Computer Science (pp. 307-321). Springer Berlin Heidelberg
  • Popescu A & Roşu G (2005) , Lecture Notes in Computer Science (pp. 331-347). Springer Berlin Heidelberg

Conference proceedings

  • Wright J, Cohen L, Rowe RNS & Popescu A (2026) . Leibniz International Proceedings in Informatics Lipics, Vol. 382
  • van Brügge J, Popescu A & Traytel D (2025) . Leibniz International Proceedings in Informatics Lipics, Vol. 352
  • Popescu A (2025) . 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) . Proceedings of the ACM on Programming Languages, Vol. 9(POPL) (pp 1687-1718)
  • Dongol B, Griffin M, Popescu A & Wright J (2024) . 2024 IEEE 37th Computer Security Foundations Symposium (CSF) (pp 403-418). Enschede, Netherlands, 8 July 2024 - 8 July 2024.
  • 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) . 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) . 12th International Conference on Interactive Theorem Proving (ITP 2021), Vol. 193 (pp 3:1-3:20). Online, 29 June 2021 - 1 July 2021.
  • (2020) . The Bulletin of Symbolic Logic, Vol. 26(3-4) (pp 312-312)
  • Popescu A & Traytel D (2019) . 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) (pp 3-21)
  • Gheri L & Popescu A (2017) . 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) . 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) . 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) . 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) . 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) . 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) . 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) (pp 234-252)
  • Blanchette JC, Popescu A & Traytel D (2015) . 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.
  • Blanchette JC, Popescu A & Traytel D (2014) (pp 46-60)
  • Kanav S, Lammich P & Popescu A (2014) (pp 167-183)
  • Blanchette JC, Popescu A & Traytel D (2014) (pp 111-127)
  • Blanchette JC, Hölzl J, Lochbihler A, Panny L, Popescu A & Traytel D (2014) (pp 93-110)
  • Popescu A, Hölzl J & Nipkow T (2013) (pp 259-275)
  • Blanchette JC & Popescu A (2013) (pp 245-260)
  • Schropp A & Popescu A (2013) (pp 114-130)
  • Popescu A, Hölzl J & Nipkow T (2013) (pp 236-252)
  • Blanchette JC, Böhme S, Popescu A & Smallbone N (2013) (pp 493-507)
  • Popescu A, Hölzl J & Nipkow T (2012) (pp 109-125)
  • Traytel D, Popescu A & Blanchette JC (2012) . 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) (pp 345-360)
  • Popescu A & Gunter EL (2011) . Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (pp 346-358)
  • Popescu A & Gunter EL (2010) (pp 109-127)
  • Popescu A, Gunter EL & Osborn CJ (2010) . 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) . Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (pp 12-20)
  • Popescu A (2009) (pp 157-172)
  • Georgescu G & Popescu A (2005) . 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) , Research Square Platform LLC.
  • Popescu A (2023) , arXiv.
  • Popescu A (2022) , arXiv.
  • Gheri L & Popescu A (2021) , arXiv.
  • Gheri L & Popescu A (2017) , arXiv.
  • Blanchette JC, Böhme S, Popescu A & Smallbone N (2016) , arXiv.
  • Blanchette JC, Popescu A & Traytel D (2015) , arXiv.
Research group

Member of the research group

Affiliate Member of the research group

Grants
  • Learning Logical Structure for a Better Proving Experience, Renaissance Philanthropy, 09/2025 - 09/2027, £328,937, as PI
  • COVERT: , EPSRC, 09/2023 – 09/2027, £ 422,585, as Co PI
  • , EPSRC, 10/2021 - 05/2025, £774,954, as Co-PI
  • Cyclic Reasoning Mechanisms for Interactive Theorem Proving, Royal Society, 08/2021 - 03/2025, £12,000, as PI
  • 2019–2020 Principal investigator for VeTSS grant “Formal Verification of Information Flow Security for Relational Databases” (£86 198)
  • 2016–2018 Principal investigator for EPSRC grant “Verification of Web-based Systems (VOWS),” acquired via the first grant scheme (£100 933)

Links

  Security of Advanced Systems research group  Foundations of Computation research group