Publications for the collection HAL LS2N-GALLINETTE for 2021
International journals with reviewing committee (ART_INT)
- [1] J. Cockx, N. Tabareau, T. Winterhalter. The Taming of the Rew: A Type Theory with Computational Assumptions. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2021.https://hal.science/hal-02901011v2
- [2] N. Tabareau, Ã. Tanter, M. Sozeau. The Marriage of Univalence and Parametricity. In Journal of the ACM (JACM) ; éd. Association for Computing Machinery, 2021, vol. 68, num. 1.https://inria.hal.science/hal-03120580v1
- [3] A. Mahboubi, T. Sibut-Pinote. A formal proof of the irrationality of ζ(3). In Logical Methods in Computer Science ; éd. Logical Methods in Computer Science Association, 2021, vol. 17, num. 1.https://inria.hal.science/hal-03517003v1
- [4] L. Birkedal, T. Dinsdale-Young, A. Guéneau, G. Jaber, K. Svendsen, N. Tzevelekos. Theorems for free from separation logic specifications. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2021, vol. 5, num. ICFP.https://hal.science/hal-03510684v1
- [5] G. Jaber, A. Murawski. Complete trace models of state and control. In ESOP 2021 - 30th European Symposium on Programming, mars 2021, Luxembourg, Luxembourg.https://hal.science/hal-03510374v1
- [6] G. Jaber, C. Riba. Temporal Refinements for Guarded Recursive Types. In ESOP 2021 - 30th European Symposium on Programming, mars 2021, Luxembourg, Luxembourg.https://hal.science/hal-03517430v1
- [7] E. Finster, A. Allioux, M. Sozeau. Types are internal infinity-groupoids. In LICS 2021, juin 2021, Rome, Italie.https://inria.hal.science/hal-03133144v2
- [8] G. Jaber, A. Murawski. Compositional relational reasoning via operational game semantics. In LICS 2021 - 36th Annual ACM/IEEE Symposium on Logic in Computer Science, juin 2021, Rome, Italie.https://hal.science/hal-03510294v1
- [9] M. Lennon-Bertrand. Complete Bidirectional Typing for the Calculus of Inductive Constructions. In ITP 2021 - 12th International Conference on Interactive Theorem Proving, juin 2021, Rome, Italie.https://hal.science/hal-03139924v2
- [10] S. Bernard, C. Cohen, A. Mahboubi, P. Strub. Unsolvability of the Quintic Formalized in Dependent Type Theory. In ITP 2021 - 12th International Conference on Interactive Theorem Proving, juin 2021, Rome / Virtual, France.https://inria.hal.science/hal-03136002v4
- [11] M. Sozeau. Touring the MetaCoq Project (Invited Paper). In LFMTP 2021 - Logical Frameworks and Meta-Languages: Theory and Practice, juillet 2021, Pittsburg, états-Unis.https://inria.hal.science/hal-03516619v1
- [12] G. Munch-Maccagnoni. Probabilistic resource limits using StatMemprof. In OCaml 2021- OCaml Users and Developers Workshop, août 2021, Online, France.https://inria.hal.science/hal-03517592v1
- [13] A. Mahboubi. Machine-checked computer-aided mathematics. https://theses.hal.science/tel-03107626v2
