| Dependent types and multi-monadic effects in F* N Swamy, C Hriþcu, C Keller, A Rastogi, A Delignat-Lavaud, S Forest, ... 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages …, 2016 | 409 | 2016 |
| Automated verification of remote electronic voting protocols in the applied pi-calculus M Backes, C Hritcu, M Maffei 21st IEEE Computer Security Foundations Symposium (CSF'08), 195-209, 2008 | 246 | 2008 |
| Software foundations BC Pierce, A Azevedo de Amorim, C Casinghino, M Gaboardi, ... Course notes, online at http://www.cis.upenn.edu/~bcpierce/sf, 2016 | 212* | 2016 |
| Verified Low-Level Programming Embedded in F* J Protzenko, JK Zinzindohoué, A Rastogi, T Ramananandro, P Wang, ... 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP), 2017 | 148 | 2017 |
| Architectural support for software-defined metadata processing U Dhawan, C Hritcu, R Rubin, N Vasilakis, S Chiricescu, JM Smith, ... Proceedings of the Twentieth International Conference on Architectural …, 2015 | 123 | 2015 |
| A verified information-flow architecture A Azevedo de Amorim, N Collins, A DeHon, D Demange, C Hritcu, ... POPL 2014, 165-178, 2014 | 118 | 2014 |
| Semantic subtyping with an SMT solver GM Bierman, AD Gordon, C Hriþcu, D Langworthy Journal of Functional Programming 22 (1), 31-105, 2012 | 110 | 2012 |
| Everest: Towards a verified, drop-in replacement of HTTPS K Bhargavan, B Bond, A Delignat-Lavaud, C Fournet, C Hawblitzel, ... 2nd Summit on Advances in Programming Languages (SNAPL 2017), 2017 | 88 | 2017 |
| Type-checking zero-knowledge M Backes, C Hritcu, M Maffei 15th ACM Conference on Computer and Communications Security (CCS 2008), 357-370, 2008 | 88 | 2008 |
| All Your IFCException Are Belong To Us C Hritcu, M Greenberg, B Karel, BC Pierce, G Morrisett 34th IEEE Symposium on Security and Privacy (Oakland 2013), 2013 | 83 | 2013 |
| Foundational Property-Based Testing Z Paraskevopoulou, C Hritcu, M Dénès, L Lampropoulos, BC Pierce 6th International Conference on Interactive Theorem Proving (ITP), 325-343, 2015 | 82 | 2015 |
| Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation C Abate, R Blanco, D Garg, C Hritcu, M Patrignani, J Thibault 32nd IEEE Computer Security Foundations Symposium (CSF), 256--271, 2019 | 79 | 2019 |
| Testing noninterference, quickly C Hritcu, J Hughes, BC Pierce, A Spector-Zabusky, D Vytiniotis, ... ACM SIGPLAN Notices 48 (9), 455-468, 2013 | 79* | 2013 |
| Dijkstra Monads for Free D Ahman, C Hritcu, K Maillard, G Martinez, G Plotkin, J Protzenko, ... 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL …, 2017 | 73 | 2017 |
| Micro-Policies: Formally Verified, Tag-Based Security Monitors A Azevedo de Amorim, M Dénes, N Giannarakis, C Hritcu, BC Pierce, ... 36th IEEE Symposium on Security and Privacy, 2015 | 73 | 2015 |
| Dijkstra monads for all K Maillard, D Ahman, R Atkey, G Martínez, C Hritcu, E Rivas, É Tanter PACMPL 3 (ICFP), 104:1– 104:29, 2019 | 61 | 2019 |
| Beginner's Luck: A Language for Property-Based Generators L Lampropoulos, D Gallois-Wong, C Hritcu, J Hughes, BC Pierce, L Xia 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017 | 58 | 2017 |
| Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation Y Juglaret, C Hritcu, AA de Amorim, B Eng, BC Pierce 29th IEEE Symposium on Computer Security Foundations (CSF), 45--60, 2016 | 49 | 2016 |
| Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms G Martínez, D Ahman, V Dumitrescu, N Giannarakis, C Hawblitzel, ... 28th European Symposium on Programming (ESOP), 30-59, 2019 | 46 | 2019 |
| Union and intersection types for secure protocol implementations M Backes, C Hritcu, M Maffei Theory of Security and Applications (TOSCA’11), 2011 | 46* | 2011 |
Benjamin C. PierceProfessor of Computer and Information Science, University of PennsylvaniaVerified email at cis.upenn.edu
