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

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)

choose your own derivative (extended abstract). - Jennifer Paykin; Antal Spector-Zabusky; Kenneth Foner (TyDe@ICFP, 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)

Ode on a random urn (functional pearl). - Leonidas Lampropoulos; Antal Spector-Zabusky; Kenneth Foner (Haskell, 2017)

Total Haskell is reasonable Coq. - Antal Spector-Zabusky; Joachim Breitner; Christine Rizkallah; Stephanie Weirich (CPP, 2018)

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Stephanie Weirich (CoRR, 2018)

Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Stephanie Weirich (Proc. ACM Program. Lang., 2018)

Embracing a mechanized formalization gap. - Antal Spector-Zabusky; Joachim Breitner; Yao Li 004; Stephanie Weirich (CoRR, 2019)

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Joshua M. Cohen; Stephanie Weirich (J. Funct. Program., 2021)