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

  • 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

  • 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

  • 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 鈥淔ormal Verification of Information Flow Security for Relational Databases鈥 (拢86 198)
  • 2016鈥2018 Principal investigator for EPSRC grant 鈥淰erification 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