Research Interests
I am interested in theoretical computer science, namely logic, type theory, and foundations of programming languages, but also different aspects of Mathematics such as algebra and topology.
I have been mostly focusing on designing typed functional programming languages and analysing the structural properties they satisfy. This lead me to investigate termination checking strategies and, more recently, a language able to model corecursive structures via copatterns.
Theses
- David Thibodeau. An Intensional Type Theory of Coinduction using Copatterns. PhD thesis. December 2020.
- David Thibodeau. Programming Infinite Structures using Copatterns. Master's thesis. December 2015.
Publications
- B. Pientka, D. Thibodeau, A. Abel, F. Ferreira and R. Zucchini. A Type Theory for Defining Logics and Proofs. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019). 2019.
- A. Momigliano, B. Pientka, and D. Thibodeau. A Case Study in Programming Coinductive Proofs: Howe's Method. In Mathematical Structures in Computer Science. 2018.
- R. Jacob-Rao, B. Pientka, and D. Thibodeau. Index-Stratified Types. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). 2018.
- David Thibodeau, Andrew Cave, Brigitte Pientka. Indexed Codata Types. 21st ACM SIGPLAN International Conference on Functional Programming (ICFP'16). 2016. (Version with appendix)
- Anton Setzer, Andreas Abel, Brigitte Pientka and David Thibodeau. Unnesting of Copatterns. Rewriting and Typed Lambda Calculi (RTA-TLCA'14). 2014.
- Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer. Copatterns: Programming Infinite Structures by Observations. 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13). 2013.
Talks
- Indexed Copatterns: Reasoning about Infinite Structures by Observations, David Thibodeau, (Joint work with Brigitte Pientka) Work in progress talk at ACM SIGPLAN Workshop on Dependently-Typed Programming (DTP'13) (slides)
- Programming and Reasoning about Coinduction using Copatterns, David Thibodeau, (Joint work with Andreas Abel, Brigitte Pientka, and Anton Setzer) Contributed talk at Workshop on Formal Meta-Theory (slides)
Other Research Work
- David Thibodeau, Termination Checking: Comparing Structural Recursion and Sized Types by Examples, Written for the class Certified Proofs and Programs taught by Brigitte Pientka in Fall 2011