Zobrazeno 1 - 10
of 141
pro vyhledávání: '"Kesner, Delia"'
We show how (well-established) type systems based on non-idempotent intersection types can be extended to characterize termination properties of functional programming languages with pattern matching features. To model such programming languages, we
Externí odkaz:
http://arxiv.org/abs/2408.11007
Several evaluation notions for lambda calculus qualify as reasonable cost models according to Slot and van Emde Boas' Invariance Thesis. A notable result achieved by Accattoli and Dal Lago is that leftmost-outermost reduction is reasonable, where the
Externí odkaz:
http://arxiv.org/abs/2404.18874
Intersection type systems have been independently applied to different evaluation strategies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been then generalized to different subsuming paradigms being able, in particular
Externí odkaz:
http://arxiv.org/abs/2404.14340
This paper studies the strength of embedding Call-by-Name ({\tt dCBN}) and Call-by-Value ({\tt dCBV}) into a unifying framework called the Bang Calculus ({\tt dBANG}). These embeddings enable establishing (static and dynamic) properties of {\tt dCBN}
Externí odkaz:
http://arxiv.org/abs/2404.12951
This paper studies the notion of meaningfulness for a unifying framework called dBang-calculus, which subsumes both call-by-name (dCbN) and call-by-value (dCbV). We first characterize meaningfulness in dBang by means of typability and inhabitation in
Externí odkaz:
http://arxiv.org/abs/2404.06361
A fundamental issue in the $\lambda$-calculus is to find appropriate notions for meaningfulness. It is well-known that in the call-by-name $\lambda$-calculus (CbN) the meaningful terms can be identified with the solvable ones, and that this notion is
Externí odkaz:
http://arxiv.org/abs/2401.12212
Autor:
Kesner, Delia, Conchúir, Shane Ó
We study Milner's lambda-calculus with partial substitutions. Particularly, we show confluence on terms and metaterms, preservation of \b{eta}-strong normalisation and characterisation of strongly normalisable terms via an intersection typing discipl
Externí odkaz:
http://arxiv.org/abs/2312.13270
We show that recent approaches of static analysis based on quantitative typing systems can be extended to programming languages with global state. More precisely, we define a call-by-value language equipped with operations to access a global memory,
Externí odkaz:
http://arxiv.org/abs/2303.08940
Publikováno v:
Logical Methods in Computer Science, Volume 20, Issue 1 (January 23, 2024) lmcs:9803
We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type
Externí odkaz:
http://arxiv.org/abs/2207.07143
Publikováno v:
Logical Methods in Computer Science, Volume 20, Issue 3 (July 29, 2024) lmcs:10901
We introduce a call-by-name lambda-calculus $\lambda Jn$ with generalized applications which is equipped with distant reduction. This allows to unblock $\beta$-redexes without resorting to the standard permutative conversions of generalized applicati
Externí odkaz:
http://arxiv.org/abs/2201.04156