Publication de la collection HAL LS2N-GALLINETTE pour 2024
Nombre de publications retournées : 14ART_INT | COMM_INT | COMM_NAT |
---|---|---|
2 | 9 | 3 |
Chiffres en cours de consolidation
Revues internationales avec comité de lecture (ART_INT)
- [1] Y. Forster, M. Sozeau, N. Tabareau. Verified Extraction from Coq to OCaml. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2024, vol. 8, num. PLDI.https://inria.hal.science/hal-04329663v1
- [2] M. Malewski, K. Maillard, N. Tabareau, Ã. Tanter. Gradual Indexed Inductive Types. In Proceedings of the ACM on Programming Languages ; éd. ACM, 2024, vol. 8, num. ICFP.https://inria.hal.science/hal-04681546v1
- [3] A. Adjedj, M. Lennon-Bertrand, K. Maillard, P. Pédrot, L. Pujet. Martin-Löf à la Coq. In CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, janvier 2024, London UK, Royaume-Uni.https://hal.science/hal-04214008v2
- [4] A. Mahboubi, M. Piquerez. A First Order Theory of Diagram Chasing. In CSL 2024 - 32nd EACSL Annual Conference on Computer Science Logic, février 2024, Naples, Italie.https://hal.science/hal-04266479v2
- [5] C. Cohen, E. Crance, A. Mahboubi. Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence. In ESOP 2024 - 33rd European Symposium on Programming, avril 2024, Luxembourg, Luxembourg.https://inria.hal.science/hal-04623207v1
- [6] L. Pujet, N. Tabareau. Observational Equality Meets CIC. In ESOP 2024 - 33rd European Symposium on Programming, avril 2024, Luxembourg, Luxembourg.https://hal.science/hal-04535982v1
- [7] M. Kerjean, P. Pédrot. $\partial$ is for Dialectica. In LICS 2024 - 39th Annual ACM/IEEE Symposium on Logic in Computer Science, juillet 2024, Tallinn, Estonie.https://inria.hal.science/hal-04583978v1
- [8] P. Pédrot. Upon This Quote I Will Build My Church Thesis. In LICS 2024 - 39th Annual ACM/IEEE Symposium on Logic in Computer Science, juillet 2024, Tallin, Estonie.https://inria.hal.science/hal-04571149v1
- [9] Y. Leray, G. Gilbert, N. Tabareau, T. Winterhalter. The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. In International Conference on Interactive Theorem Proving (ITP 2024), septembre 2024, Tbilisi, Géorgie.https://inria.hal.science/hal-04511667v2
- [10] H. Lombardi, A. Mahboubi. Geometric theories for real number algebra without sign test or dependent choice axiom. In CCC 2024 - Continuity, Computability, Constructivity From Logic to Algorithms, septembre 2024, Nice, France.https://inria.hal.science/hal-04709177v1
- [11] C. Cohen, E. Crance, A. Mahboubi. Trocq: Proof Transfer for Free, With or Without Univalence. In ESOP 2024 - 33rd European Symposium on Programming, avril 2024, Luxembourg, Luxembourg.In Stéphanie Weirich (éds.), . Springer, 2024.https://hal.science/hal-04177913v5
- [12] J. Caspar, G. Munch-Maccagnoni. Modular efficient deconstruction with typed pointer reversal. In 35es Journées Francophones des Langages Applicatifs (JFLA 2024), janvier 2024, Saint-Jacut-de-la-Mer, France.https://inria.hal.science/hal-04406342v1
- [13] M. Sozeau. MetaCoq : de la métaprogrammation à l'extraction certifiée pour Coq. In 35es Journées Francophones des Langages Applicatifs (JFLA 2024), janvier 2024, Saint-Jacut-de-la-Mer, France.https://inria.hal.science/hal-04407164v1
- [14] S. Congard. Towards a linear functional translation for borrowing. In 35es Journées Francophones des Langages Applicatifs (JFLA 2024), janvier 2024, Saint-Jacut-de-la-Mer, France.https://hal.science/hal-04360462v2