Publications associées à Simply typed lambda calculus

Degrees of Separation: A Flexible Type System for Safe Concurrency

Martin Odersky, Yichen Xu, Aleksander Slawomir Boruch-Gruszecki

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

2024

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

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

Fourier non-uniqueness sets from totally real number fields

Martin Peter Stoller

Let K be a totally real number field of degree n >= 2. The inverse different of K gives rise to a lattice in Rn. We prove that the space of Schwartz Fourier eigenfunctions on R-n which vanish on the "component-wise square root" of this lattice, is infinite ...

EUROPEAN MATHEMATICAL SOC-EMS2022

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

Unifying Analytic and Statically-Typed Quasiquotes

Christoph Koch, Amir Shaikhha, Lionel Emile Vincent Parreaux

Metaprograms are programs that manipulate (generate, analyze and evaluate) other programs. These tasks are greatly facilitated by quasiquotation, a technique to construct and deconstruct program fragments using quoted code templates expressed in the syntax ...

2018

Type Soundness Proofs with Definitional Interpreters

Tiark Rompf, Nada Amin

While type soundness proofs are taught in every graduate PL class, the gap between realistic languages and what is accessible to formal proofs is large. In the case of Scala, it has been shown that its formal model, the Dependent Object Types (DOT) calculu ...

Assoc Computing Machinery2017

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

Indicators of Evidence for Bioequivalence

Stephan Morgenthaler, Robert Staudte

Some equivalence tests are based on two one-sided tests, where in many applications the test statistics are approximately normal. We define and find evidence for equivalence in Z-tests and then one-and two-sample binomial tests as well as for t-tests. Mult ...

Mdpi Ag2016

Function Passing: A Model for Typed, Distributed Functional Programming

Heather Christine Klug, Philipp Haller, Jocelyn Boullier

The most successful systems for “big data” processing have all adopted functional APIs. We present a new programming model we call function passing designed to provide a more principled substrate on which to build data-centric distributed systems. A key id ...

Assoc Computing Machinery2016