Publications

2024

1. Formalizing Pick’s Theorem in Isabelle/HOL

   Sage Binder, and Katherine Kosaian

   In Intelligent Computer Mathematics, 2024
2. Soundly Handling Linearity

   Wenhao Tang, Daniel Hillerström, Sam Lindley, and 1 more author

   Proc. ACM Program. Lang., 2024

2023

1. Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc

   Alex Hubers, and J. Garrett Morris

   In ACM SIGPLAN International Conference on Functional Programming, ICFP’23, Seattle, WA, USA - September 5 - 8, 2023, 2023
2. A Type-Based Approach to Divide-and-Conquer Recursion in Coq

   Pedro Abreu, Benjamin Delaware, Alex Hubers, and 3 more authors

   In Proceedings of the 50th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2023, Boston, MA, USA - January 18-20, 2023, 2023

2022

1. Partial type constructors in practice

   Apoorv Ingle, Alex Hubers, and J. Garrett Morris

   In Haskell ’22: 15th ACM SIGPLAN International Haskell Symposium, Ljubljana, Slovenia, September 15 - 16, 2022, 2022

2019

1. Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)

   Burak Ekici, Arjun Viswanathan, Yoni Zohar, and 2 more authors

   In Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, 2019