Related papers: Evaluating Call-By-Need on the Control Stack
This paper concerns the explicit treatment of substitutions in the lambda calculus. One of its contributions is the simplification and rationalization of the suspension calculus that embodies such a treatment. The earlier version of this…
We show that lambda calculus is a computation model which can step by step simulate any sequential deterministic algorithm for any computable function over integers or words or any datatype. More formally, given an algorithm above a family…
In a recent paper we introduced a new framework for the study of call by need computations to normal form and root-stable form in term rewriting. Using elementary tree automata techniques and ground tree transducers we obtained simple…
We advocate the use of de Bruijn's universal abstraction $\lambda^\infty$ for the quantification of schematic variables in the predicative setting and we present a typed $\lambda$-calculus featuring the quantifier $\lambda^\infty$…
In this paper we prove that any lambda-term that is strongly normalising for beta-reduction is also strongly normalising for beta,assoc-reduction. assoc is a call-by-value rule that has been used in works by Moggi, Joachimsky, Espirito…
This paper gives a detailed account of the relationship between (a variant of) the call-by-value lambda calculus and linear logic proof nets. The presentation is carefully tuned in order to realize a strong bisimulation between the two…
We give a categorical semantics for a call-by-value linear lambda calculus. Such a lambda calculus was used by Selinger and Valiron as the backbone of a functional programming language for quantum computation. One feature of this lambda…
The so-called light logics have been introduced as logical systems enjoying quite remarkable normalization properties. Designing a type assignment system for pure lambda calculus from these logics, however, is problematic. In this paper we…
In call-by-value languages, some mutually-recursive value definitions can be safely evaluated to build recursive functions or cyclic data structures, but some definitions (let rec x = x + 1) contain vicious circles and their evaluation…
Recently, Miller and Wu introduced the positive $\lambda$-calculus, a call-by-value $\lambda$-calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs for minimal intuitionistic logic. The positive…
The fundamental lemma by Willems and coauthors facilitates a parameterization of all trajectories of a linear time-invariant system in terms of a single, measured one. This result plays an important role in data-driven simulation and…
Factorization -- a simple form of standardization -- is concerned with reduction strategies, i.e. how a result is computed. We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which…
We show that the energy required by a turbulent flow to displace a given amount of fluid through a straight duct in a given time interval can be reduced by modulating in time the pumping power. The control strategy is hybrid: it is passive,…
At the intersection of dynamical systems, control theory, and formal methods lies the construction of symbolic abstractions: these typically represent simpler, finite-state models whose behavior mimics that of an underlying concrete system…
Active regression considers a linear regression problem where the learner receives a large number of data points but can only observe a small number of labels. Since online algorithms can deal with incremental training data and take…
A demand-driven approach to program analysis have been viewed as efficient algorithms to compute only the information required to serve a target demand. In contrast, an exhaustive approach computes all information in anticipation of it…
The two Girard translations provide two different means of obtaining embeddings of Intuitionistic Logic into Linear Logic, corresponding to different lambda-calculus calling mechanisms. The translations, mapping A -> B respectively to !A -o…
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive…
We present some lambda calculus with explicit substitutions and named variables. The characteristic feature of this calculus is as follows: renaming of bound variables when performing substitutions is done using special reductions and may…
The lambda-calculus is a peculiar computational model whose definition does not come with a notion of machine. Unsurprisingly, implementations of the lambda-calculus have been studied for decades. Abstract machines are implementations…