Concept

Church encoding

Related publications (10)

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

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

Formalizing GADT constraint reasoning in Scala

Mario Bucev

Generalized algebraic data types (GADTs) are a powerful tool allowing to express invariants leveraging the type system. Scala 3 considerably improves the support of GADTs with respect to its predecessor Scala 2. A unique feature of Scala 3, compared to lan ...

2021

New Results in Integer and Lattice Programming

Christoph Hunkenschröder

An integer program (IP) is a problem of the form

\min \{f(x) : \, Ax = b, \ l \leq x \leq u, \ x \in \Z^n\}

, where

A \in \Z^{m \times n}

b \in \Z^m

l,u \in \Z^n

, and

f: \Z^n \rightarrow \Z

is a separable convex objective function. The problem o ...

EPFL2020

Measurement of the ratio of branching fractions of the decays0(2S) and arrange Lambda

Jian Wang, Olivier Schneider, Yiming Li, Yi Zhang, Aurelio Bay, Guido Haefeli, Christoph Frei, Frédéric Blanc, Tatsuya Nakada, Michel De Cian, Luca Pescatore, François Fleuret, Elena Graverini, Chitsanu Khurewathanakul, Renato Quagliani, Maria Vieites Diaz, Federico Betti, Aravindhan Venkateswaran, Luis Miguel Garcia Martin, Vitalii Lisovskyi, Mingkui Wang, Zhirui Xu, Lei Zhang, Jessica Prisciandaro, Mark Tobin, Minh Tâm Tran, Niko Neufeld, Matthew Needham, Marc-Olivier Bettler, Greig Alan Cowan, Maurizio Martinelli, Vladislav Balagura, Donal Patrick Hill, Cédric Potterat, Liang Sun, Pietro Marino, Mirco Dorigo, Jean Wicht, Xiaoxue Han, Sebastiana Gianì, Liupan An, Federico Leo Redi, Plamen Hristov Hopchev, Thibaud Humair, Maxime Schubiger, Hang Yin, Guido Andreassi, Violaine Bellée, Olivier Göran Girard, Axel Kuonen, Preema Rennee Pais, Pavol Stefko, Maria Elena Stramaglia, Tommaso Colombo, Vladimir Macko, Guillaume Max Pietrzyk, Lino Ferreira Lopes, Dipanwita Dutta, Yi Wang, Hans Dijkstra, Gerhard Raven, Peter Clarke, Frédéric Teubert, Giovanni Carboni, Victor Coco, Adam Davis, Paolo Durante, Yu Zheng, Anton Petrov, Maxim Borisyak, Feng Jiang, Zhipeng Tang, Luis Alberto Granado Cardoso, Daniel Hugo Cámpora Pérez

Using pp collisions corresponding to 3 fb integrated luminosity, recorded by the LHCb experiment at centre- of- mass energies of 7 and 8TeV, the ratio of branching fractions B (0b ! (2 S) ) =B (0b ! J= ) = 0 : 513 0 : 023 (stat) 0 : 016 (syst) 0 : 011 (B) ...

2019

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

Miniboxing: An Encoding for Specialization

Cristian Talau

In the presence of parametric polymorphism, erasure-based languages such as Java and Scala handle primitives (boolean values, integers and floating point numbers) in a suboptimal way: in order to provide a uniform representation on the low level, all primi ...

2012

On Satisfiability Modulo Computable Functions

Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal

We present a semi-decision procedure for checking satisfiability of formulas in the language of algebraic data types and integer linear arithmetic extended with user-defined terminating recursive functions. Our procedure is designed to integrate into a DPL ...

2010

Foundations for SCALA

Vincent Cremet

SCALA is an attractive programming language because it is both very expressive and statically strongly typed. This marriage against nature comes at the price of a certain complexity in the language constructs and the static analysis. This complexity makes ...

EPFL2006

Dynamic Program Parallelization

James Richard Larus

Static program analysis limits the performance improvements possible from compile-time parallelization. Dynamic program parallelization shifts a portion of the analysis from complie-time to run-time, thereby enabling optimizations whose static detection is ...

ACM1992

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.