11 citations · 24 across the 4 of their papers we have counts for
6 papers
Dedukti: a Logical Framework based on the -Calculus Modulo Theory
Ali Assaf, Guillaume Burel, Raphaël Cauderlier +7
Dedukti is a Logical Framework based on the -Calculus Modulo Theory. We show that many theories can be expressed in Dedukti: constructive and classical predicate logic, Simpl…
Making Tezos smart contracts more reliable with Coq
Bruno Bernardo, Raphaël Cauderlier, Guillaume Claret +3
Tezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. This article gives an overview of efforts using the Co…
Albert, an intermediate smart-contract language for the Tezos blockchain
Bruno Bernardo, Raphaël Cauderlier, Basile Pesin +1
Tezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. In this article we present Albert, an intermediate lan…
Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts
Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu +2
Tezos is a blockchain launched in June 2018. It is written in OCaml and supports smart contracts. Its smart contract language is called Michelson and it has been designed with form…
Mixing HOL and Coq in Dedukti (Extended Abstract)
Ali Assaf, Raphaël Cauderlier
We use Dedukti as a logical framework for interoperability. We use automated tools to translate different developments made in HOL and in Coq to Dedukti, and we combine them to pro…
Checking Zenon Modulo Proofs in Dedukti
Raphaël Cauderlier, Pierre Halmagrand
Dedukti has been proposed as a universal proof checker. It is a logical framework based on the lambda Pi calculus modulo that is used as a backend to verify proofs coming from theo…