Related papers: Linear Recursion
The article deals with a kind of recursive function templates in C++, where the recursion is realized corresponding template parameters to achieve better computational performance. Some specialization of these template functions ends the…
We introduce an intersection type system for the lambda-mu calculus that is invariant under subject reduction and expansion. The system is obtained by describing Streicher and Reus's denotational model of continuations in the category of…
Soft linear logic ([Lafont02]) is a subsystem of linear logic characterizing the class PTIME. We introduce Soft lambda-calculus as a calculus typable in the intuitionistic and affine variant of this logic. We prove that the (untyped) terms…
We address the problem of complementing higher-order patterns without repetitions of existential variables. Differently from the first-order case, the complement of a pattern cannot, in general, be described by a pattern, or even by a…
We propose a model-based approach to the model checking problem for recursive schemes. Since simply typed lambda calculus with the fixpoint operator, lambda-Y-calculus, is equivalent to schemes, we propose the use of a model of…
We introduce LAM, a subsystem of IMALL2 with restricted additive rules able to manage duplication linearly, called linear additive rules. LAM is presented as the type assignment system for a calculus endowed with copy constructors, which…
Model checking properties are often described by means of finite automata. Any particular such automaton divides the set of infinite trees into finitely many classes, according to which state has an infinite run. Building the full type…
Pattern-matching programming is an example of a rule-based programming style developed in functional languages. This programming style is intensively used in dialects of ML but is restricted to algebraic data-types. This restriction limits…
We present two theoretical results on the computation of lambda-contractive sets for linear systems with state and input constraints. First, we show that it is possible to a priori compute a number of iterations that is sufficient to…
We propose reactive Turing machines (RTMs), extending classical Turing machines with a process-theoretical notion of interaction, and use it to define a notion of executable transition system. We show that every computable transition system…
While transistor density is still increasing, clock speeds are not, motivating the search for new parallel architectures. One approach is to completely abandon the concept of CPU -- and thus serial imperative programming -- and instead to…
We describe a realizability framework for classical first-order logic in which realizers live in (a model of) typed {\lambda}{\mu}-calculus. This allows a direct interpretation of classical proofs, avoiding the usual negative translation to…
Models based on approximation capabilities have recently been studied in the context of Optimal Recovery. These models, however, are not compatible with overparametrization, since model- and data-consistent functions could then be…
Non-idempotent intersection types provide quantitative information about typed programs, and have been used to obtain time and space complexity measures. Intersection type systems characterize termination, so restrictions need to be made in…
The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called "Lambek's restriction," that is, the antecedent of any provable…
This paper formalizes and proves correct a compilation scheme for mutually-recursive definitions in call-by-value functional languages. This scheme supports a wider range of recursive definitions than previous methods. We formalize our…
Linear logic provides a framework to control the complexity of higher-order functional programs. We present an extension of this framework to programs with multithreading and side effects focusing on the case of elementary time. Our main…
This paper proposes a type-and-effect system called Teqt, which distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambda calculus with general recursion and equality types. The…
Despite a growing body of work at the intersection of deep learning and formal languages, there has been relatively little systematic exploration of transformer models for reasoning about typed lambda calculi. This is an interesting area of…
Formal mathematics and computer science proofs are formalized using Hilbert-Russell-style logical systems which are designed to not admit paradoxes and self-refencing reasoning. These logical systems are natural way to describe and reason…