Publication de la collection HAL LS2N-GALLINETTE pour 2019
Nombre de publications retournées : 15Revues internationales avec comité de lecture (ART_INT)
- [1] G. Gilbert, J. Cockx, M. Sozeau, N. Tabareau. Definitional Proof-Irrelevance without K. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2019.https://inria.hal.science/hal-01859964v2
- [2] A. Mahboubi, G. Melquiond, T. Sibut-Pinote. Formally Verified Approximations of Definite Integrals. In Journal of Automated Reasoning ; éd. Springer Verlag, 2019, vol. 62, num. 2.https://inria.hal.science/hal-01630143v2
- [3] Ã. Miquey. A Classical Sequent Calculus with Dependent Types. In ACM Transactions on Programming Languages and Systems (TOPLAS) ; éd. ACM, 2019, vol. 41, num. 2.https://inria.hal.science/hal-01519929v3
- [4] N. Tabareau, Ã. Tanter. Chemical foundations of distributed aspects. In Distributed Computing ; éd. Springer Verlag, 2019, vol. 32, num. 3.https://inria.hal.science/hal-01811884v1
- [5] P. Pédrot, N. Tabareau, H. Fehrmann, Ã. Tanter. A Reasonably Exceptional Type Theory. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2019, vol. 3.https://inria.hal.science/hal-02189128v1
- [6] M. Kerjean, J. Lemay. Higher-order distributions for differential linear logic.. In Foundations of Software Science and Computation Structures - 22nd International Conference, {FOSSACS} 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, 2019, Prague (Czech Republic), République tchèque.https://inria.hal.science/hal-01969262v2
- [7] T. Winterhalter, M. Sozeau, N. Tabareau. Eliminating Reflection from Type Theory. In CPP 2019 - 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, janvier 2019, Lisbonne, Portugal.https://hal.science/hal-01849166v3
- [8] B. Ahrens, A. Hirschowitz, A. Lafont, M. Maggesi. Modular specification of monads through higher-order presentations. In FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, juin 2019, Dortmund, Allemagne.https://hal.science/hal-02307998v1
- [9] C. Chenavier, M. Lucas. The Diamond Lemma for non-terminating rewriting systems using deterministic reduction strategies. In IWC 2019 - 8th International Workshop on Confluence, juin 2019, Dortmund, Allemagne.https://hal.science/hal-02385139v1
- [10] G. Munch-Maccagnoni, R. Douence. Efficient Deconstruction with Typed Pointer Reversal (abstract). In ML 2019 - Workshop, août 2019, Berlin, Allemagne.https://inria.hal.science/hal-02177326v2
- [11] F. Bréhard, A. Mahboubi, D. Pous. A certificate-based approach to formally verified approximations. In ITP 2019 - Tenth International Conference on Interactive Theorem Proving, septembre 2019, Portland, états-Unis.https://laas.hal.science/hal-02088529v2
- [12] T. Altenkirch, S. Boulier, A. Kaposi, N. Tabareau. Setoid type theory - a syntactic translation. In MPC 2019 - 13th International Conference on Mathematics of Program Construction, octobre 2019, Porto, Portugal.https://inria.hal.science/hal-02281225v1
- [13] A. Lafont. Signatures and models for syntax and operational semantics in the presence of variable binding. Thèses : Ecole nationale supérieure Mines-Télécom Atlantique. https://theses.hal.science/tel-03267858v1
- [14] G. Gilbert. A type theory with definitional proof-irrelevance. Thèses : Ecole nationale supérieure Mines-Télécom Atlantique. https://theses.hal.science/tel-03236271v1
- [15] I. Zhirkov, J. Cohen, R. Douence. Memory bijections: reasoning about exact memory transformations induced by refactorings in CompCert C. Rapport technique, 2019 ; LS2N, Université de Nantes.https://hal.science/hal-02078356v1