Concept

Théorème

Publications associées (43)

The PCL Theorem: Transactions cannot be Parallel, Consistent, and Live

Rachid Guerraoui, Victor Bushkov, Panagiota Fatourou

We establish a theorem called the PCL theorem, which states that it is impossible to design a transactional memory algorithm that ensures (1) parallelism, i.e., transactions do not need to synchronize unless they access the same application objects, (2) ve ...

ASSOC COMPUTING MACHINERY2019

Geometric stabilisation via $p$-adic integration

Dimitri Stelio Wyss, Michael Gröchenig

In this article we give a new proof of Ngô's Geometric Stabilisation Theorem, which implies the Fundamental Lemma. This is a statement which relates the cohomology of Hitchin fibres for a quasi-split reductive group scheme G to the cohomology of Hitchin fi ...

2018

Foundations of Implicit Function Types

Martin Odersky, Fengyun Liu, Olivier Eric Paul Blanvillain

Implicit parameters are used pervasively in Scala and are also present in a number of other programming and theorem proving languages. This paper describes a generalization of implicit parameters as they are currently found in Scala to implicit function ty ...

2017

The Myers-Steenrod Theorem For Finsler Manifolds Of Low Regularity

Marc Troyanov

We prove a version of Myers-Steenrod's theorem for Finsler manifolds under the minimal regularity hypothesis. In particular we show that an isometry between C-k,C-alpha-smooth (or partially smooth) Finsler metrics, with k + alpha > 0, k is an element of N ...

Amer Mathematical Soc2017

On some algebraic and extremal problems in discrete geometry

Seyed Hossein Nassajianmojarrad

In the present thesis, we delve into different extremal and algebraic problems arising from combinatorial geometry. Specifically, we consider the following problems. For any integer

n\ge 3

, we define

e(n)

to be the minimum positive integer such that an ...

EPFL2017

A Formally Verified NAT

George Candea, Solal Vincenzo Pirelli, Arseniy Zaostrovnykh, Luis David Figueiredo Mascarenhas Moreira Pedrosa

We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of networ ...

Assoc Computing Machinery2017

Polynomials Vanishing On Cartesian Products: The Elekes-Szabo Theorem Revisited

Frank de Zeeuw

Let F 2 C[x; y; z] be a constant-degree polynomial, and let A; B; C subset of C be finite sets of size n. We show that F vanishes on at most O(n(11/6))points of the Cartesian product A X B X C, unless F has a special group-related form. This improves a the ...

Duke Univ Press2016

Interference Functionals in Poisson Networks

Martin Haenggi

We propose and prove a theorem that allows the calculation of a class of functionals on Poisson point processes that have the form of expected values of sum-products of functions. In proving the theorem, we present a variant of the Campbell-Mecke theorem f ...

Ieee-Inst Electrical Electronics Engineers Inc2016

Projection onto the Manifold of Elongated Structures for Accurate Extraction

Pascal Fua, Vincent Lepetit, Amos Sironi

Detection of elongated structures in 2D images and 3D image stacks is a critical prerequisite in many applications and Machine Learning-based approaches have recently been shown to deliver superior performance. However, these methods essentially classify i ...

2015

L-2-cohomology and complete Hamiltonian manifolds

Tudor Ratiu

A classical theorem of Frankel for compact Kahler manifolds states that a Kahler S-1-action is Hamiltonian if and only if it has fixed points. We prove a metatheorem which says that when the Hodge theory holds on non-compact manifolds, Frankel's theorem st ...

Elsevier2015

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search