CafeSat: a Modern SAT Solver for Scala

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.

As computational thinking (CT) becomes increasingly acknowledged as an important skill in education, self-directed learning (SDL) emerges as a key strategy for developing this capability. The advent of generative AI (GenAI) conversational agents has disrup ...

Data races have long been a notorious problem in concurrent programming. They are subtle to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress ...

While software applications, programming languages, and hardware have changed, operating systems have not. Widely-used commodity operating systems are still modeled after the ones designed in the seventies. The accumulated burden of backward compatibility ...

Agent-based simulations have been widely applied in many disciplines, by scientists and engineers alike. Scientists use agent-based simulations to tackle global problems, including alleviating poverty, reducing violence, and predicting the impact of pandem ...

The Dependent Object Type (DOT) calculus was designed to put Scala on a sound basis, but while DOT relies on structural subtyping, Scala is a fundamentally class-based language. This impedance mismatch means that a proof of DOT soundness by itself is ...

This paper studies the problem of online performance optimization of constrained closed-loop control systems, where both the objective and the constraints are unknown black-box functions affected by exogenous time-varying contextual disturbances. A primal- ...

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

Many programming languages in the OO tradition now support pattern matching in some form. Historical examples include Scala and Ceylon, with the more recent additions of Java, Kotlin, TypeScript, and Flow. But pattern matching on generic class hierarchies ...

Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents match types ...

It's been a little more than 40 years since researchers first suggested exploiting quantum physics to build more powerful computers. During this time, we have seen the development of many quantum algorithms and significant technological advances to make th ...

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

Universal quantum algorithms that prepare arbitrary n-qubit quantum states require O(2n) gate complexity. The complexity can be reduced by considering specific families of quantum states depending on the task at hand. In particular, multipartite quantum st ...

We present an automated approach to verify the correctness of programming assignments, such as the ones that arise in a functional programming course. Our approach takes as input student submissions and reference solutions, and uses equivalence checking to ...

Programming has changed; programming languages have not. Modern software embraced reusable software components, i.e., public libraries, and runs in the cloud, on machines that co-locate applications from various origins. This new programming paradigm leads ...

Programming with monads can be advantageous even in imperative languages with builtin support for side effects. However, in these languages composing monadic programs is different from composing side effecting imperative programs. This does not need to be ...

We propose a flow for automated quantum compila- tion. Our flow takes a Boolean function implemented in Python as input and translates it into a format appropriate for reversible logic synthesis. We focus on two quantum compilation tasks: uniform state pre ...

Adiabatic quantum-flux-parametron (AQFP) circuits are a family of superconducting electronic (SCE) circuits that have recently gained growing interest due to their low-energy consumption, and may serve as alternative technology to overcome the down-scaling ...

Many natural optimization problems are NP-hard, which implies that they are probably hard to solve exactly in the worst-case. However, it suffices to get reasonably good solutions for all (or even most) instances in practice. This paper presents a new algo ...

A key open question in quantum computing is whether quantum algorithms can potentially offer a significant advantage over classical algorithms for tasks of practical interest. Understanding the limits of classical computing in simulating quantum systems is ...

Machine intelligence greatly impacts almost all domains of our societies. It is profoundly changing the field of mechanical engineering with new technical possibilities and processes. The education of future engineers also needs to adapt in terms of techni ...

CafeSat: a Modern SAT Solver for Scala

Chattez avec Graph Search

Generative AI-Enabled Conversational Interaction to Support Self-Directed Learning Experiences in Transversal Computational Thinking

Degrees of Separation: A Flexible Type System for Safe Concurrency

Dynamic Linkers Are the Narrow Waist of Operating Systems

Generalizing Bulk-Synchronous Parallel Processing for Data Science: From Data to Threads and Agent-Based Simulations

Type-Preserving Compilation of Class-Based Languages

Primal-Dual Contextual Bayesian Optimization for Control System Online Optimization with Time-Average Constraints

Scaling Language Features for Program Verification

A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning

Type-Level Programming with Match Types

Practical Compilation of Quantum Programs

NP Satisfiability for Arrays as Powers

Efficient Preparation of Cyclic Quantum States

Proving and Disproving Equivalence of Functional Programming Assignments

Trust as a Programming Primitive

Representing Monads with Capabilities

From Boolean functions to quantum circuits: A scalable quantum compilation flow in C++

Algebraic and Boolean Optimization Methods for AQFP Superconducting Circuits

Learning from survey propagation: a neural network for MAX-E-3-SAT

Classical variational simulation of the Quantum Approximate Optimization Algorithm

Automated Design: A Journey Across Modelling, Optimization, and Education