Concept

Lambda cube

Publications associées (25)

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

New York2022

On the probability distribution of the local times of diagonally operator-self-similar Gaussian fields with stationary increments

Thomas Mountford, Kamran Kalbasi

In this paper, we study the local times of vector-valued Gaussian fields that are 'diagonally operator-selfsimilar' and whose increments are stationary. Denoting the local time of such a Gaussian field around the spatial origin and over the temporal unit h ...

INT STATISTICAL INST2020

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

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

Chiral charge erasure via thermal fluctuations of magnetic helicity

Eray Sabancilar

We consider a relativistic plasma of fermions coupled to an Abelian gauge field and carrying a chiral charge asymmetry, which might arise in the early Universe through baryogenesis. It is known that on large length scales, lambda greater than or similar to ...

Iop Publishing Ltd2016

Minkowski space is locally the Noldus limit of Poisson process causets

Jan Cristina

A Poisson process P-lambda on R-d with causal structure inherited from the the usual Minkowski metric on R-d has a normalised discrete causal distance D-lambda (x, y) given by the height of the longest causal chain normalised by lambda(1/d)c(d). We prove t ...

Iop Publishing Ltd2016

On Satisfiability for Quantified Formulas in Instantiation-Based Procedures

Viktor Kuncak, Nicolas Charles Yves Voirol

Procedures for first-order logic with equality are used in many modern theorem provers and solvers, yet procedure termination in case of interesting sub-classes of satisfiable formulas remains a challenging problem. We present an instantiation-based semi-d ...

2016

MAGIC observations of the February 2014 flare of 1ES 1011+496 and ensuing constraint of the EBL density

Thomas Günther Bretz

Context. During February-March 2014, the MAGIC telescopes observed the high-frequency peaked BL Lac 1ES 1011 + 496 (z = 0.212) in flaring state at very-high energy (VHE, E > 100 GeV). The flux reached a level of more than ten times higher than any previous ...

Edp Sciences S A2016

Additional Material for "Unifying Data Representation Transformations"

Vlad Ureche

This report shows an attempt to formalize the data representation transformation mechanism in the ``Unifying Data Representation Transformations'' paper. Since the mechanism described in the paper is targeted at the Scala programming language and the speci ...

2014

Complete Completion using Types and Weights

Viktor Kuncak, Tihomir Gvero, Ivan Kuraj, Ruzica Piskac

Developing modern software typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that synthesizes ...

ACM2013

Graph Chatbot

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.

Connectez-vous pour utiliser Chat avec Graph Search