Unité

Laboratoire d'analyse et de raisonnement automatisés

Laboratoire

Publications associées (1 000)

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

A positive combinatorial formula for symplectic Kostka-Foulkes polynomials I: Rows

Thomas Gerber

We prove a conjecture of Lecouvey, which proposes a closed, positive combinatorial formula for symplectic Kostka-Foulkes polynomials, in the case of rows of arbitrary weight. To show this, we construct a new algorithm for computing cocyclage in terms of wh ...

ACADEMIC PRESS INC ELSEVIER SCIENCE2020

Barriers to the net zero target in personal mobility

Philippe Thalmann

What are the barriers on the way to zero-emissions personal mobility (ZEM)? Based on the world cafe discussion with experts from the ETH domain, two main sets of barriers arise: a first set related to the difficulties of organising ZEM, a second set relate ...

2020

In Via Accidit

Alexandre Blanc, Marco Bakker

To share an event that happened or could have happen on the road in relation to architecture or space in a wider sense. ...

MANSLAB2020

Individual change and self-tracking

Alexandre André Robert Rigal

The Quantified Self (QS) members explore the relation between self-tracking and individual change. Berger and Luckmann insists that individual change begins with a disruptive emotion. It continues with the public sharing of the story of the event. Then the ...

2020

Packing the Boolean lattice with copies of a poset

Istvan Tomon

The Boolean lattice (2[n],subset of) is the family of all subsets of [n]={1,MIDLINE HORIZONTAL ELLIPSIS,n}, ordered by inclusion. Let P be a partially ordered set. We prove that if n is sufficiently large, then there exists a packing P of copies of P in (2 ...

WILEY2020

Exact DAG-Aware Rewriting

Mathias Soeken, Heinz Riener

We present a generic resynthesis framework for optimizing Boolean networks parameterized with a multi-level logic representation, a cut-computation algorithm, and a resynthesis algorithm. The framework allows us to realize powerful optimization algorithms ...

IEEE2020

CHIMERA: Combining Ring-LWE-based Fully Homomorphic Encryption Schemes

Dimitar Petkov Jetchev

This paper proposes a practical hybrid solution for combining and switching between three popular Ring-LWE-based FHE schemes: TFHE, B/FV and HEAAN. This is achieved by first mapping the different plaintext spaces to a common algebraic structure and then by ...

WALTER DE GRUYTER GMBH2020

A Mechanized Theory of Quoted Code Patterns

The pattern matching on code from the new macro system of Scala 3 is modeled by a calculus called λ half-circle. We present a mechanized proof of soundness of the calculus in Coq and discuss encountered challenges. ...

2020

Scaling Functional Synthesis and Repair

Emmanouil Koukoutos

Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the soft ...

EPFL2019

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