Publications associées à Théorème de complétude de Gödel

Orthologic with Axioms

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

Association for Computing Machinery2024

The completeness of the generalized eigenfunctions and an upper bound for the counting function of the transmission eigenvalue problem for Maxwell equations

Hoài-Minh Nguyên, Jean Louis-Alexandre Fornerod

Cakoni and Nguyen recently proposed very general conditions on the coefficients of Maxwell equations for which they established the discreten ess of the set of eigenvalues of the transmission problem and studied their locations. In this paper, we establish ...

2021

Verified Functional Programming

Nicolas Charles Yves Voirol

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solve ...

EPFL2019

Sound Proof of Proximity of Knowledge

Serge Vaudenay

Public-key distance bounding schemes are needed to defeat relay attacks in payment systems. So far, only five such schemes exist, but fail to fully protect against malicious provers. In this paper, we solve this problem. We provide a full formalism to defi ...

2015

An overview of the Leon verification system: verification by translation to recursive functions

Viktor Kuncak, Etienne Kneuss, Philippe Paul Henri Suter, Régis William Blanc

We present the Leon verification system for a subset of the Scala programming language. Along with several functional features of Scala, Leon supports imperative constructs such as mutations and loops, using a translation into recursive functional form. Bo ...

2013

Omnidirectional Light Field Analysis and Reconstruction

Luigi Bagnato

Digital photography exists since 1975, when Steven Sasson attempted to build the first digital camera. Since then the concept of digital camera did not evolve much: an optical lens concentrates light rays onto a focal plane where a planar photosensitive ar ...

EPFL2012

Capabilities for Uniqueness and Borrowing

Martin Odersky, Philipp Haller

An important application of unique object references is safe and efficient message passing in concurrent object-oriented programming. However, to prevent the ill effects of aliasing, practical systems often severely restrict the shape of messages passed by ...

Springer2010

Control of the Toycopter using a Flat Approximation

Dominique Bonvin, Philippe Müllhaupt, Jean Lévine

This paper considers a helicopter-like setup called the Toycopter. Its particularities reside first in the fact that the toycopter motion is constrained to remain on a sphere and second in the use of a variable rotational speed of the propellers to vary th ...

2008

Survivable Routing of Mesh Topologies in IP-over-WDM Networks by Recursive Graph Contraction

Patrick Thiran, Maciej Kurant

Failure restoration at the IP layer in IP-over-WDM networks requires to map the IP topology on the WDM topology in such a way that a failure at the WDM layer leaves the IP topology connected. Such a mapping is called survivable. Finding a survivable mappin ...

2007