-
Semi-automatic verification of cryptographic primitives
CertiCrypt is a framework that enables the machine-checked construction and verification of cryptographic proofs in the Coq proof assistant. CertiCrypt instruments the... -
The Flow Caml System: Documentation and user's manual
Flow Caml is an extension of the Objective Caml language with a type system tracing information flow. Its purpose is basically to allow to write ``real'' programs and... -
Une analyse syntaxique d'ASN.1 : 1990 en Caml Light
ASN.1 est un langage de spécification de protocoles normalisé par l'ISO et utilisé fréquemment dans les télécommunications. Il permet de décrire et de regrouper en... -
ReCaml: execution state as the cornerstone of reconfigurations
International audience -
an intuitionistic lambda calculus with exceptions
We introduce a typed lambda-calculus which allows the use of exceptions in the ML style. It is an extension of the system AF2 of Krivine & Leivant (Krivine, 1990;...
