Publications related to Parametric polymorphism

When Subtyping Constraints Liberate A Novel Type Inference Approach for First-Class Polymorphism

Lionel Emile Vincent Parreaux, Aleksander Slawomir Boruch-Gruszecki

Type inference in the presence of first-class or "impredicative" second-order polymorphism a la System F has been an active research area for several decades, with original works dating back to the end of the 80s. Yet, until now many basic problems remain ...

Assoc Computing Machinery2024

Formal Foundations of Capture Tracking

Aleksander Slawomir Boruch-Gruszecki

Type systems are a device for verifying properties of programs without running them. Many programming languages used in the industry have always had a type system, while others were initially created without a type system and later adopted one, when the ad ...

EPFL2024

Semantic Shape Editing with Parametric Implicit Templates

Uday Kusupati

We propose a semantic shape editing method to edit 3D triangle meshes using parametric implicit surface templates, benefiting from the many advantages offered by analytical implicit representations, such as infinite resolution and boolean or blending opera ...

ACM Association for Computing Machinery2024

Design Space Exploration for Partitioning Dataflow Program on CPU-GPU Heterogeneous System

Marco Mattavelli, Simone Casale Brunet, Aurélien François Gilbert Bloch

Dataflow programming is a methodology that enables the development of high-level, parametric programs that are independent of the underlying platform. This approach is particularly useful for heterogeneous platforms, as it eliminates the need to rewrite ap ...

SPRINGER2023

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

Alpha-NML Universal Predictors

Michael Christoph Gastpar, Marco Bondaschi

Inspired by Sibson’s alpha-mutual information, we introduce a new parametric class of universal predictors. This class interpolates two well-known predictors, the mixture estimator, that includes the Laplace and the Krichevsky-Trofimov predictors, and the ...

2022

A Baseline Cellular Antiviral State Is Maintained by cGAS and Its Most Frequent Naturally Occurring Variant rs610913

Jacques Fellay, Christian Axel Wandall Thorball, Shuting Xu

Upon recognition of aberrantly located DNA, the innate immune sensor cyclic GMP-AMP synthase (cGAS) activates stimulator of IFN genes (STING)/IFN regulatory factor (IRF)3-driven antiviral responses. In this study, we characterized the ability of a specific ...

American Association of Immunologists ; Oxford University Press2022

Adaptation of hepatitis C virus to interferon lambda polymorphism across multiple viral genotypes

Jacques Fellay, Nimisha Chaturvedi

Genetic polymorphism in the interferon lambda (IFN-lambda) region is associated with spontaneous clearance of hepatitis C virus (HCV) infection and response to interferon-based treatment. Here, we evaluate associations between IFN-l polymorphism and HCV va ...

2019

Refutation-based synthesis in SMT

Viktor Kuncak, Andrew Joseph Reynolds

We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided ...

SPRINGER2019

Entropy as a tool for crystal discovery

Pablo Miguel Piaggi

The computational prediction of crystal structures has emerged as an useful alternative to expensive and often cumbersome experiments. We propose an approach to the prediction of crystal structures and polymorphism based on reproducing the crystallization ...

EPFL2019

Predicting polymorphism in molecular crystals using orientational entropy

Pablo Miguel Piaggi, Michele Parrinello

We introduce a computational method to discover polymorphs in molecular crystals at finite temperature. The method is based on reproducing the crystallization process starting from the liquid and letting the system discover the relevant polymorphs. This id ...

National Academy of Sciences2018

Higher-Order Subtyping with Type Intervals

Sandro Stucki

Modern, statically typed programming languages provide various abstraction facilities at both the term- and type-level. Common abstraction mechanisms for types include parametric polymorphism -- a hallmark of functional languages -- and subtyping -- which ...

EPFL2017

Java and Scala's Type Systems are Unsound The Existential Crisis of Null Pointers

Nada Amin

We present short programs that demonstrate the unsoundness of Java and Scala's current type systems. In particular, these programs provide parametrically polymorphic functions that can turn any type into any type without (down) casting. Fortunately, parame ...

Assoc Computing Machinery2016

Contextualized ranking of entity types based on knowledge graphs

Karl Aberer, Philippe Cudré-Mauroux, Michele Catasta, Roman Prokofyev

A large fraction of online queries targets entities. For this reason, Search Engine Result Pages (SERPs) increasingly contain information about the searched entities such as pictures, short summaries, related entities, and factual information. A key facet ...

Elsevier Science Bv2016

Implementing Higher-Kinded Types in Dotty

Martin Odersky, Guillaume André Fradji Martres, Dmytro Petrashko

dotty is a new, experimental Scala compiler based on DOT, the calculus of Dependent Object Types. Higher-kinded types are a natural extension of first-order lambda calculus, and have been a core construct of Haskell and Scala. As long as such types are jus ...

ACM2016

Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers

Nada Amin

We present short programs that demonstrate the unsoundness of Java and Scala’s current type systems. In particular, these programs provide parametrically polymorphic functions that can turn any type into any type without (down)casting. Fortunately, paramet ...

2015

Search Techniques for Code Generation

Tihomir Gvero

This dissertation explores techniques that synthesize and generate program fragments and test inputs. The main goal of these techniques is to improve and support automation in program synthesis and test input generation. This is important because performin ...

EPFL2015

KEu(MoO4)(2): Polymorphism, Structures, and Luminescent Properties

Alla Arakcheeva, Philip Pattison

In this paper, with the example of two different polymorphs of KEu(MoO4)(2), the influence of the ordering of the A-cations on the luminescent properties in scheelite related compounds (A',A '') (B',B '')O-4 is investigated. The polymorphs were synthe ...

American Chemical Society2015

Genome-wide association study of virologic response with efavirenz-containing or abacavir-containing regimens in AIDS clinical trials group protocols

Paul Jack Mc Laren

Background Efavirenz and abacavir are components of recommended first-line regimens for HIV-1 infection. We used genome-wide genotyping and clinical data to explore genetic associations with virologic failure among patients randomized to efavirenz-containi ...

Lippincott Williams & Wilkins2015

Counterexample-Guided Quantifier Instantiation for Synthesis in SMT, Computer Aided Verification

Viktor Kuncak, Andrew Joseph Reynolds

We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided ...

2015