Publications associées à Constructive set theory

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

Dagstuhl, Germany, Schloss Dagstuhl - Leibniz-Zentrum fur Informatik2023

Extractable Witness Encryption for the Homogeneous Linear Equations Problem

Serge Vaudenay, Bénédikt Minh Dang Tran

Witness encryption is a cryptographic primitive which encrypts a message under an instance of an NP language and decrypts the ciphertext using a witness associated with that instance. In the current state of the art, most of the witness encryption construc ...

Springer2023

Shared metadata for data-centric materials science

Giovanni Pizzi, Ronald Earle Miller, Gian-Marco Rignanese, Carsten Baldauf, Matthias Scheffler, Tristan Bereau

The expansive production of data in materials science, their widespread sharing and repurposing requires educated support and stewardship. In order to ensure that this need helps rather than hinders scientific work, the implementation of the FAIR-data prin ...

Nature Portfolio2023

Impact of Redundancy on Resilience in Distributed Optimization and Learning

Nirupam Gupta, Shuo Liu

This paper considers the problem of resilient distributed optimization and stochastic learning in a server-based architecture. The system comprises a server and multiple agents, where each agent has its own local cost function. The agents collaborate with ...

Assoc Computing Machinery2023

Collective data-based drawings A common ground for adaptive contributive design

The laboratory ALICE (Atelier de la Conception de l’Espace) at the École Polytechnique Fédérale de Lausanne (EPFL) advances a comprehensive approach to data-based drawing oriented towards architectural and urban co-design processes. This drawing methodolog ...

2023

Positive Definite Completions and Continuous Graphical Models

Kartik Waghmare

This thesis concerns the theory of positive-definite completions and its mutually beneficial connections to the statistics of function-valued or continuously-indexed random processes, better known as functional data analysis. In particular, it dwells upon ...

EPFL2023

Formula Normalizations in Verification

Viktor Kuncak, Simon Guilloud, Mario Bucev, Dragana Milovancevic

We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem ...

2023

NP Satisfiability for Arrays as Powers

Viktor Kuncak, Rodrigo Raya

We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is inNP. As an application, we extend the combinatory array logic fragmentto handle cardinality constraints. The resulting fragme ...

Springer, Cham2022

INCLASS: Incremental Classification Strategy for Self-Aware Epileptic Seizure Detection

David Atienza Alonso, Giovanni Ansaloni, Tomas Teijeiro Campo, Renaud Marquis

Wearable Health Companions allow the unobtrusive monitoring of patients affected by chronic conditions. In particular, by acquiring and interpreting bio-signals, they enable the detection of acute episodes in cardiac and neurological ailments. Nevertheless ...

IEEE2022

Discrete Voss surfaces: Designing geodesic gridshells with planar cladding panels

Corentin Jean Dominique Fivet, Nicolas Robin Montagne, Olivier Baverel

The design and construction of doubly-curved structures often reveals to be challenging and can result in complex manufacturing and assembly. A recent strategy to tackle this difficulty consists in exploiting the connection between discrete differential ge ...

2022

Learning to Generate the Unknowns as a Remedy to the Open-Set Domain Shift

Mathieu Salzmann

In many situations, the data one has access to at test time follows a different distribution from the training data. Over the years, this problem has been tackled by closed-set domain adaptation techniques. Recently, open-set domain adaptation has emerged ...

IEEE COMPUTER SOC2022

Les Cahiers de l'Ibois 2 / Ibois Notebooks 2

Yves Weinand

The second Ibois Notebook focuses its reflections on the Grand-Chalet station project in Rossinière. Christophe Catsaros and Tadashi Ono carry out a landscape analysis in text and image around the idea of a revival of the alpine vernacular. Isabel Concheir ...

EPFL PRESS2021

Financing Biomedical Ventures - Myths and Realities

Jeffrey Scott Behrens

Angel funding is an important source of capital for startup ventures (J. Sohl 2019), providing a similar level of capital as institutional venture capital (OECD 2011). But angel funding is challenging to study due to the informal nature of the activity. A ...

EPFL2020

Microstructural controls of anticrack nucleation in highly porous brittle solids

Johan Alexandre Philippe Gaume, Henning Löwe, Jonas Ritter

Porous brittle solids have the ability to collapse and fail even under compressive stresses. In fracture mechanics, this singular behavior, often referred to as anticrack, demands for appropriate continuum models to predict the catastrophic failure. To ide ...

Nature Research2020

chi-Shell, a new spatial deployable lattice compared to traditional reticulated shells

Mark Pauly, Florin Isvoranu, Etienne Bouleau, Francis Julian Panetta

The chi-Shells is a new kind of deployable reticulated shells that has features comparable to other traditional shells. Its deployment uses the mechanical properties of a beam grid to generate a three-dimensional shape. This new generation of reticulated s ...

INT CENTER NUMERICAL METHODS ENGINEERING2019

Forbidden induced subposets of given height

Istvan Tomon

Let P be a partially ordered set. The function La* (n, P) denotes the size of the largest family F subset of 2([n]) that does not contain an induced copy of P. It was proved by Methuku and Palvolgyi that there exists a constant C-P (depending only on P) su ...

ACADEMIC PRESS INC ELSEVIER SCIENCE2019

X-Shell, a new spatial deployable lattice compared to traditional reticulated shells

Mark Pauly, Florin Isvoranu, Francis Julian Panetta, Etienne Bouleau

The χ-Shells is a new kind of deployable reticulated shells that has features comparable to other traditional shells. Its deployment uses the mechanical properties of a beam grid to generate a three-dimensional shape. This new generation of reticulated she ...

International Association for Shell and Spatial Structures (IASS)2019

35 years of photovoltaics: Analysis of the TISO-10-kW solar plant, lessons learnt in safety and performance-Part 1

Christophe Ballif, Alessandro Francesco Aldo Virtuani, Eleonora Annigoni

The TISO-10-kW solar plant, connected to the grid in 1982, is the oldest installation of this kind in Europe. Its history is well documented, and the full set of modules has been tested indoors at regular intervals over the years. After 35 years of operati ...

WILEY2019

Transport à câble aérien en milieu urbain: pertinence et pratique

Fernando Anisio De Oliveira Simas

The intense urbanization of cities has left few options when it comes to insert large mobility infrastructure they need to move their inhabitants. A surface rail network, a dedicated roadway bus line or any other mobility infrastructure such as a tramway a ...

EPFL2019

How little does non-exact recovery help in group testing?

Volkan Cevher, Jonathan Mark Scarlett

We consider the group testing problem, in which one seeks to identify a subset of defective items within a larger set of items based on a number of tests. We characterize the information-theoretic performance limits in the presence of list decoding, in whi ...

Ieee2017