Copatterns: programming infinite structures by observations A Abel, B Pientka, D Thibodeau, A Setzer ACM SIGPLAN Notices 48 (1), 27-38, 2013 | 192 | 2013 |
A type theory for defining logics and proofs B Pientka, D Thibodeau, A Abel, F Ferreira, R Zucchini 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-13, 2019 | 30* | 2019 |
Indexed codata types D Thibodeau, A Cave, B Pientka Proceedings of the 21st ACM SIGPLAN International Conference on Functional …, 2016 | 26 | 2016 |
Unnesting of copatterns A Setzer, A Abel, B Pientka, D Thibodeau Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA …, 2014 | 18 | 2014 |
A case study in programming coinductive proofs: Howe’s method A Momigliano, B Pientka, D Thibodeau Mathematical structures in computer science 29 (8), 1309-1343, 2019 | 15* | 2019 |
Index-stratified types R Jacob-Rao, B Pientka, D Thibodeau 3rd International Conference on Formal Structures for Computation and …, 2018 | 13 | 2018 |
Programming infinite structures using copatterns D Thibodeau Master’s thesis, McGill University, 2015 | 5 | 2015 |
An Intensional Type Theory of Coinduction using Copatterns D Thibodeau PhD thesis, McGill University, 2020 | 2 | 2020 |
An intensional type theory of coinduction with copatterns D Thibodeau McGill University, 2021 | | 2021 |
Termination Checking: Comparing Structural Recursion and Sized Types by Examples D Thibodeau | | |