Decision Procedures for Algebraic Data Types with Abstractions

Related publications (27)

About
Privacy
Disclaimer

Graph Chatbot

Type-Level Programming with Match Types

Martin Odersky, Olivier Eric Paul Blanvillain

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

ASSOC COMPUTING MACHINERY2022

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

Yichen Xu, Lionel Emile Vincent Parreaux, Aleksander Slawomir Boruch-Gruszecki

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

Assoc Computing Machinery2022

Failure and success of the spectral bias prediction for Laplace Kernel Ridge Regression: the case of low-dimensional data

Matthieu Wyart, Umberto Maria Tomasini, Antonio Sclocchi

Recently, several theories including the replica method made predictions for the generalization error of Kernel Ridge Regression. In some regimes, they predict that the method has a 'spectral bias': decomposing the true function f* on the eigenbasis of the ...

JMLR-JOURNAL MACHINE LEARNING RESEARCH2022

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

Virtual ADTs for Portable Metaprogramming

Martin Odersky, Nicolas Alexander Stucki

Scala 3 provides a metaprogramming interface that represents the abstract syntax tree definitions using algebraic data types. To allow the compiler to freely evolve without breaking the metaprogramming interface, we present virtual algebraic data types (or ...

ASSOC COMPUTING MACHINERY2021

On the stress tensor light-ray operator algebra

Grégoire Olivier Mathys, Matthew Thomas Walters, Alexandre Mathieu Frédéric Belin

We study correlation functions involving generalized ANEC operators of the form integral dx-x-n+2T--x -> in four dimensions. We compute two, three, and ...

Springer Nature2021

Contact networks across ages: computational analysis of epidemiological dynamics

Gianrocco Lazzari

For decades mathematical modeling in epidemiology has helped understanding the dynamics of infectious diseases, as well as describe possible intervention scenarios to prevent and control them. However, such models were relying on several assumptions, such ...

EPFL2020

Synthesis of Flexible Accelerators for Early Adoption of Ring-LWE Post-quantum Cryptography

Francesco Regazzoni, Subhadeep Banik, Hamid Nejatollahi

The advent of the quantum computer makes current public-key infrastructure insecure. Cryptography community is addressing this problem by designing, efficiently implementing, and evaluating novel public-key algorithms capable of withstanding quantum comput ...

ASSOC COMPUTING MACHINERY2020

Multi-omics reveals abundant mitochondrial genomic and circadian expression variation in the Drosophila Genetic Reference Panel

Maria Litovchenko

Modern biology rapidly generates a wealth of data,which can only be analysed computationally.Despite the variety of available data types,most of them aim to provide an answer to one question: how does genotypic diversity translates into phenotypes? This qu ...

EPFL2020

DELF: Safeguarding deletion correctness in Online Social Networks

Georgios Damaskinos

Deletion is a core facet of Online Social Networks (OSNs). For users, deletion is a tool to remove what they have shared and control their data. For OSNs, robust deletion is both an obligation to their users and a risk when developer mistakes inevitably oc ...

USENIX ASSOC2020

Page 2 of 3