output
20052026
most citedPhotonic microwave signals with zeptosecond level absolute timing noise

447 citations

researchers with a paper here
collaborating institutions
Showing cs.LOShow all

8 papers · 1 filter

cs.LO2023★ 6 cited

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…

cs.LO2016

A verified abstract machine for functional coroutines

Tristan Crolard

Functional coroutines are a restricted form of control mechanism, where each coroutine is represented with both a continuation and an environment. This restriction was originally o…

cs.LO2015★ 4 cited

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…

cs.LO2015★ 12 cited

Translating HOL to Dedukti

Ali Assaf, Guillaume Burel

Dedukti is a logical framework based on the lambda-Pi-calculus modulo rewriting, which extends the lambda-Pi-calculus with rewrite rules. In this paper, we show how to translate th…

cs.LO2015★ 1 cited

Recovering Intuition from Automated Formal Proofs using Tableaux with Superdeduction

David Delahaye, Mélanie Jacquel

We propose an automated deduction method which allows us to produce proofs close to the human intuition and practice. This method is based on tableaux, which generate more natural…

cs.LO2014

Impossibility of Gathering, a Certification

Pierre Courtieu, Lionel Rieg, Xavier Urbain +1

Recent advances in Distributed Computing highlight models and algorithms for autonomous swarms of mobile robots that self-organise and cooperate to solve global objectives. The ove…