Concept

Lambda calculus

Related publications (127)

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.

A Mechanized Theory of the Box Calculus

Yichen Xu

Capture calculus is an extension of System Fsub that tracks free variables of terms in their type, allowing one to represent capabilities while limiting their scope. While previous calculi had mechanized soundness proofs, the latest version, namely the box ...

2023

Architecture and Abstraction

Pier Vittorio Aureli

In this theoretical study of abstraction in architecture—the first of its kind—Pier Vittorio Aureli argues for a reconsideration of abstraction, its meanings, and its sources. Although architects have typically interpreted abstraction in formal terms—the p ...

The MIT Press2023

Capturing Types

Martin Odersky, Aleksander Slawomir Boruch-Gruszecki, Ondrej Lhoták

Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties could be guaranteed if one knew the free variables captured by values. We describe CC

New York2023

Short homology bases for hyperelliptic hyperbolic surfaces

Given a hyperelliptic hyperbolic surface S of genus g >= 2, we find bounds on the lengths of homologically independent loops on S. As a consequence, we show that for any lambda is an element of (0, 1) there exists a constant N(lambda) such that every such ...

Jerusalem2023

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

Macro Annotations for Scala 3

Zhendong Ang

Macro annotations are an important feature in Scala 2 macro system. Many projects use macro annotations to implement their systems or libraries. Due to the unportability of Scala 2 macro system, Scala 3 redesigns the macro system to make it more reliable a ...

2022

Type-preserving compilation of (most of) FGJ into DOT

Guillaume André Fradji Martres

The Dependent Object Type (DOT) calculus was designed to put Scala on a sound basis, but while DOT relies on structural subtyping, Scala is a fundamentally class-based language. This impedance mismatch means that a proof of DOT soundness by itself is not e ...

2022

Revisiting the General Identifiability Problem

Negar Kiyavash, Ehsan Mokhtarian, Yaroslav Kivva, Seyed Jalal Etesami

We revisit the problem of general identifiability originally introduced in [Lee et al., 2019] for causal inference and note that it is necessary to add positivity assumption of observational distribution to the original definition of the problem. We show t ...

2022

On the Modeling of Organic Electrochemical Transistors

Matteo Cucchi

Due to their synaptic functionality based on interacting electronic and ionic charge carriers, organic electrochemical transistors (OECTs) appeal as highly attractive candidates for a new generation of organic neuromorphic devices. Despite their acknowledg ...

SPIE-INT SOC OPTICAL ENGINEERING2022

Tuned hybrid nonuniform subdivision surfaces with optimal convergence rates

Xiaodong Wei

This article presents an enhanced version of our previous work, hybrid nonuniform subdivision (HNUS) surfaces, to achieve optimal convergence rates in isogeometric analysis (IGA). We introduce a parameter lambda (14

WILEY2021