Designing a Multi-Precision number Theory Library. - Catalin Hritcu; Iulian Goriac; Raluca Mihaela Gordan; Elena Erbiceanu (Int. J. Comput., 2003)

A Reference Implementation of ADF (Agent Developing Framework): Semantic Web-Based Agent Communication. - Catalin Hritcu; Sabin C. Buraga (SYNASC, 2005)

Type-checking zero-knowledge. - Michael Backes 001; Catalin Hritcu; Matteo Maffei (CCS, 2008)

Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus. - Michael Backes 001; Catalin Hritcu; Matteo Maffei (CSF, 2008)

Achieving Security Despite Compromise Using Zero-knowledge. - Michael Backes 001; Martin P. Grochulla; Catalin Hritcu; Matteo Maffei (CSF, 2009)

A Step-indexed Semantics of Imperative Objects - Catalin Hritcu; Jan Schwinghammer (Log. Methods Comput. Sci., 2009)

Automatically Verifying Typing Constraints for a Data Processing Language. - Michael Backes 001; Catalin Hritcu; Thorsten Tarrach (CPP, 2011)

Union and Intersection Types for Secure Protocol Implementations. - Michael Backes 001; Catalin Hritcu; Matteo Maffei (TOSCA, 2011)

On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols. - Michael Backes 001; Alex Busenius; Catalin Hritcu (NASA Formal Methods, 2012)

Hardware Support for Safety Interlocks and Introspection. - Udit Dhawan; Albert Kwon; Edin Kadric; Catalin Hritcu; Benjamin C. Pierce; Jonathan M. Smith; André DeHon; Gregory Malecha; Greg Morrisett; Thomas F. Knight Jr.; Andrew Sutherland; Tom Hawkins; et al. (SASO Workshops, 2012)

Semantic subtyping with an SMT solver. - Gavin M. Bierman; Andrew D. Gordon 001; Catalin Hritcu; David E. Langworthy (J. Funct. Program., 2012)

Union, intersection, and refinement types and reasoning about type disjointness for security protocol analysis. - Catalin Hritcu (2012)

Testing noninterference, quickly. - Catalin Hritcu; John Hughes 001; Benjamin C. Pierce; Antal Spector-Zabusky; Dimitrios Vytiniotis; Arthur Azevedo de Amorim; Leonidas Lampropoulos (ICFP, 2013)

All Your IFCException Are Belong to Us. - Catalin Hritcu; Michael Greenberg 002; Ben Karel; Benjamin C. Pierce; Greg Morrisett (IEEE Symposium on Security and Privacy, 2013)

Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations. - Michael Backes 001; Catalin Hritcu; Matteo Maffei (J. Comput. Secur., 2014)

Architectural Support for Software-Defined Metadata Processing. - Udit Dhawan; Catalin Hritcu; Raphael Rubin; Nikos Vasilakis; Silviu Chiricescu; Jonathan M. Smith; Thomas F. Knight Jr.; Benjamin C. Pierce; André DeHon (ASPLOS, 2015)

Micro-Policies: Formally Verified, Tag-Based Security Monitors. - Catalin Hritcu (PLAS@ECOOP, 2015)

Foundational Property-Based Testing. - Zoe Paraskevopoulou; Catalin Hritcu; Maxime Dénès; Leonidas Lampropoulos; Benjamin C. Pierce (ITP, 2015)

Micro-Policies: Formally Verified, Tag-Based Security Monitors. - Arthur Azevedo de Amorim; Maxime Dénès; Nick Giannarakis; Catalin Hritcu; Benjamin C. Pierce; Antal Spector-Zabusky; Andrew Tolmach (IEEE Symposium on Security and Privacy, 2015)

Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components. - Yannis Juglaret; Catalin Hritcu; Arthur Azevedo de Amorim; Benjamin C. Pierce; Antal Spector-Zabusky; Andrew Tolmach (CoRR, 2015)

The Joint EasyCrypt-F*-CryptoVerif School 2014. - Catalin Hritcu (ACM SIGLOG News, 2015)

Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. - Yannis Juglaret; Catalin Hritcu; Arthur Azevedo de Amorim; Boris Eng; Benjamin C. Pierce (CSF, 2016)

Dependent types and multi-monadic effects in F. - Nikhil Swamy; Catalin Hritcu; Chantal Keller; Aseem Rastogi; Antoine Delignat-Lavaud; Simon Forest; Karthikeyan Bhargavan; Cédric Fournet; Pierre-Yves Strub; Markulf Kohlweiss; Jean Karim Zinzindohoue; Santiago Zanella-Béguelin (POPL, 2016)

Dijkstra Monads for Free. - Danel Ahman; Catalin Hritcu; Guido Martínez; Gordon D. Plotkin; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy (CoRR, 2016)

Beyond Full Abstraction: Formalizing the Security Guarantees of Low-Level Compartmentalization. - Yannis Juglaret; Catalin Hritcu; Arthur Azevedo de Amorim; Benjamin C. Pierce (CoRR, 2016)

A verified information-flow architecture. - Arthur Azevedo de Amorim; Nathan Collins; André DeHon; Delphine Demange; Catalin Hritcu; David Pichardie; Benjamin C. Pierce; Randy Pollack; Andrew Tolmach (J. Comput. Secur., 2016)

Testing noninterference, quickly. - Catalin Hritcu; Leonidas Lampropoulos; Antal Spector-Zabusky; Arthur Azevedo de Amorim; Maxime Dénès; John Hughes 001; Benjamin C. Pierce; Dimitrios Vytiniotis (J. Funct. Program., 2016)

Dijkstra monads for free. - Danel Ahman; Catalin Hritcu; Kenji Maillard; Guido Martínez; Gordon D. Plotkin; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy (POPL, 2017)

Beginner's luck: a language for property-based generators. - Leonidas Lampropoulos; Diane Gallois-Wong; Catalin Hritcu; John Hughes 001; Benjamin C. Pierce; Li-yao Xia (POPL, 2017)

Everest: Towards a Verified, Drop-in Replacement of HTTPS. - Karthikeyan Bhargavan; Barry Bond; Antoine Delignat-Lavaud; Cédric Fournet; Chris Hawblitzel; Catalin Hritcu; Samin Ishtiaq; Markulf Kohlweiss; K. Rustan M. Leino; Jay R. Lorch; Kenji Maillard; Jianyang Pan; et al. (SNAPL, 2017)

Verified Low-Level Programming Embedded in F*. - Jonathan Protzenko; Jean Karim Zinzindohoué; Aseem Rastogi; Tahina Ramananandro; Peng Wang 048; Santiago Zanella-Béguelin; Antoine Delignat-Lavaud; Catalin Hritcu; Karthikeyan Bhargavan; Cédric Fournet; Nikhil Swamy (CoRR, 2017)

A Monadic Framework for Relational Verification (Functional Pearl). - Niklas Grimm; Kenji Maillard; Cédric Fournet; Catalin Hritcu; Matteo Maffei; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin (CoRR, 2017)

Formally Secure Compilation of Unsafe Low-Level Components (Extended Abstract). - Guglielmo Fachini; Catalin Hritcu; Marco Stronati; Ana Nora Evans; Théo Laurent; Arthur Azevedo de Amorim; Benjamin C. Pierce; Andrew Tolmach (CoRR, 2017)

Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract). - Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Marco Stronati; David Swasey (CoRR, 2017)

Verified low-level programming embedded in F. - Jonathan Protzenko; Jean Karim Zinzindohoué; Aseem Rastogi; Tahina Ramananandro; Peng Wang 048; Santiago Zanella-Béguelin; Antoine Delignat-Lavaud; Catalin Hritcu; Karthikeyan Bhargavan; Cédric Fournet; Nikhil Swamy (Proc. ACM Program. Lang., 2017)

When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. - Carmine Abate; Arthur Azevedo de Amorim; Roberto Blanco; Ana Nora Evans; Guglielmo Fachini; Catalin Hritcu; Théo Laurent; Benjamin C. Pierce; Marco Stronati; Andrew Tolmach (CCS, 2018)

A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. - Niklas Grimm; Kenji Maillard; Cédric Fournet; Catalin Hritcu; Matteo Maffei; Jonathan Protzenko; Tahina Ramananandro; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin (CPP, 2018)

The Meaning of Memory Safety. - Arthur Azevedo de Amorim; Catalin Hritcu; Benjamin C. Pierce (POST, 2018)

Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier. - Guido Martínez; Danel Ahman; Victor Dumitrescu; Nick Giannarakis; Chris Hawblitzel; Catalin Hritcu; Monal Narasimhamurthy; Zoe Paraskevopoulou; Clément Pit-Claudel; Jonathan Protzenko; Tahina Ramananandro; Aseem Rastogi; et al. (CoRR, 2018)

Exploring Robust Property Preservation for Secure Compilation. - Carmine Abate; Roberto Blanco; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Jérémy Thibault (CoRR, 2018)

Secure Compilation (Dagstuhl Seminar 18201). - Amal Ahmed 001; Deepak Garg 001; Catalin Hritcu; Frank Piessens (Dagstuhl Reports, 2018)

Recalling a witness: foundations and applications of monotonic state. - Danel Ahman; Cédric Fournet; Catalin Hritcu; Kenji Maillard; Aseem Rastogi; Nikhil Swamy (Proc. ACM Program. Lang., 2018)

The Quest for Formally Secure Compartmentalizing Compilation. - Catalin Hritcu (2019)

Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. - Carmine Abate; Roberto Blanco; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Jérémy Thibault (CSF, 2019)

Meta-F ^ star : Proof Automation with SMT, Tactics, and Metaprograms. - Guido Martínez; Danel Ahman; Victor Dumitrescu; Nick Giannarakis; Chris Hawblitzel; Catalin Hritcu; Monal Narasimhamurthy; Zoe Paraskevopoulou; Clément Pit-Claudel; Jonathan Protzenko; Tahina Ramananandro; Aseem Rastogi; et al. (ESOP, 2019)

Trace-Relating Compiler Correctness and Secure Compilation. - Carmine Abate; Roberto Blanco; Stefan Ciobaca; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Éric Tanter; Jérémy Thibault (CoRR, 2019)

Dijkstra monads for all. - Kenji Maillard; Danel Ahman; Robert Atkey; Guido Martínez; Catalin Hritcu; Exequiel Rivas; Éric Tanter (Proc. ACM Program. Lang., 2019)

Luck: A Probabilistic Language for Testing. - Leonidas Lampropoulos; Benjamin C. Pierce; Li-yao Xia; Diane Gallois-Wong; Catalin Hritcu; John Hughes 001 (Foundations of Probabilistic Programming, 2020)

Trace-Relating Compiler Correctness and Secure Compilation. - Carmine Abate; Roberto Blanco; Stefan Ciobaca; Adrien Durier; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Éric Tanter; Jérémy Thibault (ESOP, 2020)

The next 700 relational program logics. - Kenji Maillard; Catalin Hritcu; Exequiel Rivas; Antoine Van Muylder (Proc. ACM Program. Lang., 2020)

Dynamic IFC Theorems for Free! - Maximilian Algehed; Jean-Philippe Bernardy; Catalin Hritcu (CSF, 2021)

Secure Compilation (Dagstuhl Seminar 21481). - David Chisnall; Deepak Garg 001; Catalin Hritcu; Mathias Payer (Dagstuhl Reports, 2021)

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. - Carmine Abate; Philipp G. Haselwarter; Exequiel Rivas; Antoine Van Muylder; Théo Winterhalter; Catalin Hritcu; Kenji Maillard; Bas Spitters (IACR Cryptol. ePrint Arch., 2021)

An Extended Account of Trace-relating Compiler Correctness and Secure Compilation. - Carmine Abate; Roberto Blanco; Stefan Ciobaca; Adrien Durier; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Éric Tanter; Jérémy Thibault (ACM Trans. Program. Lang. Syst., 2021)

SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation. - Akram El-Korashy; Roberto Blanco; Jérémy Thibault; Adrien Durier; Deepak Garg 001; Catalin Hritcu (CSF, 2022)

Securely Compiling Verified F* Programs With IO. - Cezar-Constantin Andrici; Catalin Hritcu; Guido Martínez; Exequiel Rivas; Théo Winterhalter (CoRR, 2023)

The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. - Philipp G. Haselwarter; Benjamin Salling Hvass; Lasse Letager Hansen; Théo Winterhalter; Catalin Hritcu; Bas Spitters (IACR Cryptol. ePrint Arch., 2023)

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. - Philipp G. Haselwarter; Exequiel Rivas; Antoine Van Muylder; Théo Winterhalter; Carmine Abate; Nikolaj Sidorenco; Catalin Hritcu; Kenji Maillard; Bas Spitters (ACM Trans. Program. Lang. Syst., 2023)

SECOMP: Formally Secure Compilation of Compartmentalized C Programs. - Jérémy Thibault; Roberto Blanco; Dongjae Lee; Sven Argo; Arthur Azevedo de Amorim; Aïna Linn Georges; Catalin Hritcu; Andrew Tolmach (CCS, 2024)

Securing Verified IO Programs Against Unverified Code in F. - Cezar-Constantin Andrici; Stefan Ciobaca; Catalin Hritcu; Guido Martínez; Exequiel Rivas; Éric Tanter; Théo Winterhalter (Proc. ACM Program. Lang., 2024)

FSLH: Flexible Mechanized Speculative Load Hardening. - Jonathan Baumann; Roberto Blanco; Léon Ducruet; Sebastian Harwig; Catalin Hritcu (CSF, 2025)

FSLH: Flexible Mechanized Speculative Load Hardening. - Roberto Blanco; Léon Ducruet; Sebastian Harwig; Catalin Hritcu (CoRR, 2025)

SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F. - Cezar-Constantin Andrici; Danel Ahman; Catalin Hritcu; Ruxandra Icleanu; Guido Martínez; Exequiel Rivas; Théo Winterhalter (CoRR, 2025)

Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs. - Jérémy Thibault; Joseph Lenormand; Catalin Hritcu (CoRR, 2025)