Author of the publication

Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems.

, , , , , , and . MKM/Calculemus/DML, volume 7961 of Lecture Notes in Computer Science, page 359-363. Springer, (2013)

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

The Implicit Calculus of Constructions as a Programming Language with Dependent Types., and . FoSSaCS, volume 4962 of Lecture Notes in Computer Science, page 365-379. Springer, (2008)A generalization of the Takeuti-Gandy interpretation., , and . Math. Struct. Comput. Sci., 25 (5): 1071-1099 (2015)Environments and the complexity of abstract machines., and . PPDP, page 4-16. ACM, (2017)Verification of the Interface of a Small Proof System in Coq.. TYPES, volume 1512 of Lecture Notes in Computer Science, page 28-45. Springer, (1996)Using linear codes as a fault countermeasure for nonlinear operations: application to AES and formal verification., , , and . J. Cryptogr. Eng., 7 (1): 75-85 (2017)Programming and Computing in HOL.. TPHOLs, volume 1869 of Lecture Notes in Computer Science, page 17-37. Springer, (2000)Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory., and . LFMTP, volume 332 of EPTCS, page 54-67. (2020)The Negligible and Yet Subtle Cost of Pattern Matching., and . APLAS, volume 10695 of Lecture Notes in Computer Science, page 426-447. Springer, (2017)Sets in Coq, Coq in Sets.. J. Formaliz. Reason., 3 (1): 29-48 (2010)On the Role of Type Decorations in the Calculus of Inductive Constructions., and . CSL, volume 3634 of Lecture Notes in Computer Science, page 151-166. Springer, (2005)