The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
Traditionally, calculi of explicit substitution [1] have been conceived as an implementation technique for β-reduction and studied with the tools of rewriting theory. This computational view has been extremely fruitful (see [2] for a recent survey) and raises the question if there may also be a more abstract underlying logical foundation.
In this presentation we give an overview of Dual Light Affine Logic (DLAL), a polymorphic type system for lambda calculus ensuring that typable lambda terms are executable in polynomial time. We stress the importance of proof-nets from Light linear logic for the design of this type system and for a result establishing that typable lambda-terms can be evaluated efficiently with optimal reduction. We...
A type system for the lambda-calculus enriched with recursive and corecursive functions over equi-inductive and -coinductive types is presented in which all well-typed programs are strongly normalizing. The choice of equi-inductive types, instead of the more common iso-inductive types, influences both reduction rules and the strong normalization proof. By embedding iso- into equi-types, the latter...
We define an effective, sound and complete game semantics for , Intuitionistic Arithmetic with ω-rule. Our semantics is equivalent to the original semantics proposed by Lorentzen [6] , but it is based on the more recent notions of ”backtracking” ([5],[2] ) and of isomorphism between proofs and strategies ([8]). We prove that winning strategies in our game semantics...
Safety is a syntactic condition of higher-order grammars that constrains occurrences of variables in the production rules according to their type-theoretic order. In this paper, we introduce the safe lambda calculus, which is obtained by transposing (and generalizing) the safety condition to the setting of the simply-typed lambda calculus. In contrast to the original definition of safety, our calculus...
Refinement calculi are program logics which formalize the “top-down” methodology of software development promoted by Dijkstra and Wirth in the early days of structured programming. I present here the shallow embedding of a refinement calculus into constructive type theory. This embedding involves monad transformers and the computational reflexion of weakest-preconditions, using a continuation...
We describe a new method to represent (partial) recursive functions in type theory. For every recursive definition, we define a co-inductive type of prophecies that characterises the traces of the computation of the function. The structure of a prophecy is a possibly infinite tree, which is coerced by linearisation to a type of partial results defined by applying the delay monad to the co-domain of...
We give an arithmetical proof of the strong normalization of the λ-calculus (and also of the λμ-calculus) where the type system is the one of simple types with recursive equations on types. The proof using candidates of reducibility is an easy extension of the one without equations but this proof cannot be formalized in Peano arithmetic. The strength of the system needed for such a proof was...
The lambda-Pi-calculus allows to express proofs of minimal predicate logic. It can be extended, in a very simple way, by adding computation rules. This leads to the lambda-Pi-calculus modulo. We show in this paper that this simple extension is surprisingly expressive and, in particular, that all functional Pure Type Systems, such as the system F, or the Calculus of Constructions, can be embedded in...
In 1994 Herbelin started and partially achieved the programme of showing that, for intuitionistic implicational logic, there is a Curry-Howard interpretation of sequent calculus into a variant of the λ-calculus, specifically a variant which manipulates formally “applicative contexts” and inverts the associativity of “applicative terms”. Herbelin worked with a fragment of sequent calculus with constraints...
The intuitionistic fragment of the call-by-name version of Curien and Herbelin’s -calculus is isolated and proved strongly normalising by means of an embedding into the simply-typed λ-calculus. Our embedding is a continuation-and-garbage-passing style translation, the inspiring idea coming from Ikeda and Nakazawa’s translation of Parigot’s λμ-calculus. The...
We analyze in game-semantical terms the finitary fragment of the linear π-calculus. This calculus was introduced by Yoshida, Honda, and Berger [NYB01], and then refined by Honda and Laurent [LH06]. The features of this calculus - asynchrony and locality in particular - have a precise correspondence in Game Semantics. Building on work by Varacca and Yoshida [VY06], we interpret π-processes in...
In the first part of the paper I investigate categorical models of multiplicative biadditive intuitionistic linear logic, and note that in them some surprising coherence laws arise. The thesis for the second part of the paper is that these models provide the right framework for investigating differential structure in the context of linear logic. Consequently, within this setting, I introduce a notion...
We give a many-one reduction of the set of true sentences to the set of consequences of the λ-calculus with the ω-rule. This solves in the affirmative a long-standing problem of H. Barendregt (1975).
In our previous work [17] we have shown that for any ω-algebraic meet-cpo D, if all higher-order stable function spaces built from D are ω-algebraic, then D is finitary. This accomplishes the first of a possible, two-step process in solving the problem raised in [1,2]: whether the category of stable bifinite domains of Amadio-Droste-Göbel [1,6] is the largest cartesian closed full sub-category within...
Initial algebra semantics is a cornerstone of the theory of modern functional programming languages. For each inductive data type, it provides a fold combinator encapsulating structured recursion over data of that type, a Church encoding, a build combinator which constructs data of that type, and a fold/build rule which optimises modular programs by eliminating intermediate data of that type. It has...
We propose type systems that abstractly interpret small-step rather than big-step operational semantics. We treat an expression or evaluation context as a structure in a linear logic with hypothetical reasoning. Evaluation order is not only regulated by familiar focusing rules in the operational semantics, but also expressed by structural rules in the type system, so the types track control flow more...
We prove that the inhabitation problem for rank two intersection types is decidable, but (contrary to a common belief) EXPTIME-hard. The exponential time hardness is shown by reduction from the in-place acceptance problem for alternating Turing machines.
Inspired by recent work on normalisation by evaluation for sums, we propose a normalising and confluent extensional rewriting theory for the simply-typed λ-calculus extended with sum types. As a corollary of confluence we obtain decidability for the extensional equational theory of simply-typed λ-calculus extended with sum types. Unlike previous decidability results, which rely on advanced rewriting...
A Kripke Semantics is defined for a higher-order logic programming language with constraints, based on Church’s Theory of Types and a generic constraint formalism. Our syntactic formal system, hoHH() (higher-order hereditary Harrop formulas with constraints), which extends λProlog’s logic, is shown sound and complete. A Kripke semantics for equational reasoning in the...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.