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 coinductive objects via copatterns.
- Anton Setzer, Andreas Abel, Brigitte Pientka and David Thibodeau. Unnesting of Copatterns, Rewriting and Typed Lambda Calculi (RTA-TLCA'14)
- 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)
- 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