Positive Higher−Order Queries by Benedikt, M, Puppis, G, Vu, H

“…We investigate a higher-order query language that embeds operators of the positive relational algebra within the simply-typed Lambda-calculus. Our language allows one to succinctly define ordinary positive relational algebra queries (conjunctive queries and unions of conjunctive queries) and, in addition, second-order query functionals, which allow the transformation of CQs and UCQs in a generic (i.e., syntax independent) way. …”

Psi-calculi: a framework for mobile processes with nominal data and logic by Jesper Bengtson, Magnus Johansson, Joachim Parrow, Björn Victor

“…Psi-calculi can be even more general, for example by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and predicate logic for assertions. …”
Get full text

A Graph Model for Imperative Computation by Guy McCusker

“…This new notion of graph gives rise to a model of affine lambda-calculus that admits an interpretation of imperative constructs including variable assignment, dereferencing and allocation. …”
Get full text

Cartesian Difference Categories by Mario Alvarez-Picallo, Jean-Simon Pacaud Lemay

“…Important models of Cartesian differential categories include classical differential calculus of smooth functions and categorical models of the differential $\lambda$-calculus. However, Cartesian differential categories cannot account for other interesting notions of differentiation of a more discrete nature such as the calculus of finite differences. …”
Get full text

Prioritise the Best Variation by Wen Kokke, Ornela Dardha

“…Similarly, in Good Variation (GV)$-$a linear concurrent $\lambda$-calculus$-$deadlock freedom is guaranteed by combining channel creation and thread spawning under the same operation, called fork. …”
Get full text

Circular Proofs as Session-Typed Processes: A Local Validity Condition by Farzaneh Derakhshan, Frank Pfenning

“…Proof theory provides a foundation for studying and reasoning about programming languages, most directly based on the well-known Curry-Howard isomorphism between intuitionistic logic and the typed lambda-calculus. More recently, a correspondence between intuitionistic linear logic and the session-typed pi-calculus has been discovered. …”
Get full text

Perspectives by Asudeh, A, Giorgolo, G

“…Our formalization is a conservative extension of the simply-typed lambda calculus utilizing monads, a construction in category theory that provides a way to map a set of objects and functions into a more complex space of objects and functions. …”

A Sorted Semantic Framework for Applied Process Calculi by Johannes Borgström, Ramūnas Gutkovas, Joachim Parrow, Björn Victor, Johannes Åman Pohjola

“…We also demonstrate different notions of computation on data terms, including cryptographic primitives and a lambda-calculus with erratic choice. Finally, we prove standard congruence and structural properties of bisimulation; the proof has been machine-checked using Nominal Isabelle in the case of a single name sort.…”
Get full text

Statman's Hierarchy Theorem by Bram Westerbaan, Bas Westerbaan, Rutger Kuyper, Carst Tankink, Remy Viehoff, Henk Barendregt

“…In the Simply Typed $\lambda$-calculus Statman investigates the reducibility relation $\leq_{\beta\eta}$ between types: for $A,B \in \mathbb{T}^0$, types freely generated using $\rightarrow$ and a single ground type $0$, define $A \leq_{\beta\eta} B$ if there exists a $\lambda$-definable injection from the closed terms of type $A$ into those of type $B$. …”
Get full text

Computably Based Locally Compact Spaces by Paul Taylor

“…ASD (Abstract Stone Duality) is a re-axiomatisation of general topology in which the topology on a space is treated, not as an infinitary lattice, but as an exponential object of the same category as the original space, with an associated lambda-calculus. In this paper, this is shown to be equivalent to a notion of computable basis for locally compact sober spaces or locales, involving a family of open subspaces and accompanying family of compact ones. …”
Get full text

Revisiting Call-by-value B\"ohm trees in light of their Taylor expansion by Emma Kerinec, Giulio Manzonetto, Michele Pagani

“…The call-by-value lambda calculus can be endowed with permutation rules, arising from linear logic proof-nets, having the advantage of unblocking some redexes that otherwise get stuck during the reduction. …”
Get full text

On Berry's conjectures about the stable order in PCF by Fritz Müller

“…PCF is a sequential simply typed lambda calculus language. There is a unique order-extensional fully abstract cpo model of PCF, built up from equivalence classes of terms. …”
Get full text

The syntactic side of autonomous categories enriched over generalised metric spaces by Fredrik Dahlqvist, Renato Neves

“…Our main result is the introduction of a V-equational deductive system for linear {\lambda}-calculus together with a proof that it is sound and complete. …”
Get full text

LAMBDA: The Ultimate Declarative by Steele, Guy Lewis, Jr.

“…Procedurally defined data structures may compi le into code as good as would be expected for data defined by the more usual declarative means. 3.) Lambda-calculus-theoretic models of such constructs as GOT, DO loops, call-by-name, etc. may be used directly as macros, the expansion of which may then compile into code as good as that produced by compilers which are designed especially to handle GOTO, DO, etc. …”
Get full text

Compositional lexical networks: a case study of the English spatial adjectives by Worthing, D

“…I argue that a traditional approach to formal semantics based on the simply-typed lambda calculus is not rich enough to implement lexical networks because it is unable to type the arrows which link word senses together. …”

Presentable signatures and initial semantics by Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, Marco Maggesi

“…Our (presentable) signatures subsume classical algebraic signatures (i.e., signatures for languages with variable binding, such as the pure lambda calculus) and extend them to include several other significant examples of syntactic constructions. …”
Get full text

A Logical Foundation for Environment Classifiers by Takeshi Tsukada, Atsushi Igarashi

“…In this paper, we investigate the Curry-Howard isomorphism for environment classifiers by developing a typed {\lambda}-calculus {\lambda}|>. It corresponds to multi-modal logic that allows quantification by transition variables---a counterpart of classifiers---which range over (possibly empty) sequences of labeled transitions between possible worlds. …”
Get full text

Extended Initiality for Typed Abstract Syntax by Benedikt Ahrens

“…Afterwards we specify, via the category-theoretic iteration operator, translations from PCF to the untyped lambda calculus.…”
Get full text

Temperley–lieb algebra: from knot theory to logic and computation via quantum mechanics by Abramsky, S

“…Finally, we interpret a non-commutative lambda calculus (a variant of the Lambek calculus, widely used in computational linguistics) in the Temperley-Lieb category, and thus show how diagrammatic simplification can be viewed as functional computation. …”

Abstract interpretation of domain-specific embedded languages by Backhouse, K, Kevin Stuart Backhouse

“…</p><p>In this dissertation, DSELs and their signatures are encoded using the polymorphic lambda calculus. This allows the correctness of the abstract interpretation of DSELs to be proved using the parametricity theorem: safety is derived for free from the polymorphic type of a program. …”