Building a Calculus of Data Structures

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

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 ...

We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based p ...

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

We study the hitting probabilities of the solution to a system of d stochastic heat equations with additive noise subject to Dirichlet boundary conditions. We show that for any bounded Borel set with positive (d-6)\documentclass[12pt]{minimal} \usepackage{ ...

Image information about the state of a building after an earthquake, which can be collected without endangering the post-earthquake reconnaissance activities, can be used to reduce uncertainties in response predictions for future seismic events. This paper ...

In this article, we propose a dynamical system to avoid obstacles which are star shaped and simultaneously converge to a goal. The convergence is almost-global in a domain and the stationary points are identified explicitly. Our approach is based on the id ...

We discuss two extensions to a recently introduced theory of arrays, which are based on considerations coming from the model theory of power structures. First, we discuss how the ordering relation on the index set can be expressed succinctly by referring t ...

We consider the problem of comparing several samples of stochastic processes with respect to their second-order structure, and describing the main modes of variation in this second order structure, if present. These tasks can be seen as an Analysis of Vari ...

Technology mapping transforms a technology-independent representation into a technology-dependent one given a library of cells. This process is performed by means of local replacements that are extracted by matching sections of the subject graph to library ...

Decision-making permeates every aspect of human and societal development, from individuals' daily choices to the complex decisions made by communities and institutions. Central to effective decision-making is the discipline of optimization, which seeks th ...

Logic rewriting is a powerful optimization technique that replaces small sections of a Boolean network with better implementations. Typically, exact synthesis is used to compute optimum replacement on-the-fly, with possible support for Boolean don't cares. ...

Let F be a family of n pairwise intersecting circles in the plane. We show that the number of lenses, that is convex digons, in the arrangement induced by F is at most 2n - 2. This bound is tight. Furthermore, if no two circles in F touch, then the geometr ...

Genes implicated in translation control have been associated with autism spectrum disorders (ASDs). However, some important genetic causes of autism, including the 16p11.2 microdeletion, bear no obvious connection to translation. Here, we use proteomics, g ...

Two -particle Bose-Einstein momentum correlation functions are studied for charged-hadron pairs in lead -lead collisions at a center -of -mass energy per nucleon pair of .'/sNN = 5.02 TeV. The data sample, containing 4.27 x 109 minimum bias events correspo ...

Genome-wide chromatin conformation capture assays provide formidable insights into the spatial organization of genomes. However, due to the complexity of the data structure, their integration in multi-omics workflows remains challenging. We present data st ...

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 ...

This article explores how the logic underlying modal practices tends to modulate the population’s responsiveness to improvements in global transport supply. Based on a quantitative survey conducted in 2018–2019 among the working population of the cantons o ...

Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties could be guaranteed if one knew the free variables captured by values. We describe CC

In this paper, we consider the first eigenvalue.1(O) of the Grushin operator.G :=.x1 + |x1|2s.x2 with Dirichlet boundary conditions on a bounded domain O of Rd = R d1+ d2. We prove that.1(O) admits a unique minimizer in the class of domains with prescribed ...

Graph Neural Networks (GNNs) have emerged as a powerful tool for learning on graphs, demonstrating exceptional performance in various domains. However, as GNNs become increasingly popular, new challenges arise. One of the most pressing is the need to ensur ...

Building a Calculus of Data Structures

Chat with Graph Search

Orthologic with Axioms

Interpolation and Quantifiers in Ortholattices

Automated Formal Verification of Software Network Functions

Hitting with Probability One for Stochastic Heat Equations with Additive Noise

Reducing uncertainties in response predictions of earthquake-damaged masonry buildings using data from image-based inspection

Dynamical system approach to navigation around obstacles

Succinct ordering and aggregation constraints in algebraic array theories

Transportation-based functional ANOVA and PCA for covariance operators

In Medio Stat Virtus: Combining Boolean and Pattern Matching

Reliable data-driven decision-making through optimal transport

Scalable Logic Rewriting Using Don’t Cares

A Note on Lenses in Arrangements of Pairwise Intersecting Circles in the Plane

The autism susceptibility kinase, TAOK2, phosphorylates eEF2 and modulates translation

Two-particle Bose-Einstein correlations and their Lévy parameters in PbPb collisions at √sNN=5.02 TeV

Orchestrating chromosome conformation capture analysis with Bioconductor

LISA – A Modern Proof System

Analysing the potential for modal shiftbased on the logic of modal choice

Capturing Types

The first Grushin eigenvalue on cartesian product domains

Privacy-Preserving Machine Learning on Graphs