Author of the publication

Trocq: Proof Transfer for Free, With or Without Univalence.

, , and . ESOP (1), volume 14576 of Lecture Notes in Computer Science, page 239-268. Springer, (2024)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

A bargain for mergesorts (functional pearl) - How to prove your mergesort correct and stable, almost for free., and . CoRR, (2024)Measure Construction by Extension in Dependent Type Theory with Application to Integration., and . CoRR, (2022)The MetaCoq Project., , , , , , , , and . J. Autom. Reason., 64 (5): 947-999 (2020)Unsolvability of the Quintic Formalized in Dependent Type Theory., , , and . ITP, volume 193 of LIPIcs, page 8:1-8:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2021)Semantics of Probabilistic Programs using s-Finite Kernels in Coq., , and . CPP, page 3-16. ACM, (2023)Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description)., , and . FSCD, volume 167 of LIPIcs, page 34:1-34:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2020)Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence., , and . ESOP (1), volume 14576 of Lecture Notes in Computer Science, page 269-274. Springer, (2024)Trocq: Proof Transfer for Free, With or Without Univalence., , and . ESOP (1), volume 14576 of Lecture Notes in Computer Science, page 239-268. Springer, (2024)Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle., , , , and . ITP, volume 141 of LIPIcs, page 13:1-13:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2019)Measure Construction by Extension in Dependent Type Theory with Application to Integration., and . J. Autom. Reason., 67 (3): 28 (September 2023)