Home » Team publications


Publications  for  the  collection  HAL LS2N-GALLINETTE  for  2024

Total of the publications found : 13

Overview of LS2N-GALLINETTE publications by types
ART_INT
COMM_INT
COMM_NAT
283

Chiffres en cours de consolidation

International journals with reviewing committee (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

International conferences with reviewing committee (COMM_INT)

    • [3] 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
    • [4] 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
    • [5] 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
    • [6] 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
    • [7] 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
    • [8] 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
    • [9] 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
    • [10] 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

National conferences with reviewing committee (COMM_NAT)

    • [11] 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
    • [12] 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
    • [13] 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
Copyright : LS2N 2017 - Legal notices - 
 -