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.
We introduce a simple translation from λ-calculus to combinatory logic (cl) such that: A is an SN λ-term iff the translation result of A is an SN term of cl (the reductions are β-reduction in λ-calculus and weak reduction in cl). None of the conventional translations from λ-calculus to CL satisfy the above property. Our translation provides a simpler SN proof of Gödel's λ-calculus by the ordinal number...
We introduce S2, a typed intermediate language for vectors, based on a 2-level type-theory, which distinguishes between compile-time and run-time. The paper shows how S2 can be used to extract useful information from programs written in the Nested Sequence Calculus NSC, an idealized high-level parallel calculus for nested sequences. We study two translations from NSC to S2. The most interesting shows...
In this paper we study programs written in a purely functional language with Data Types. We introduce a class of redundant code, the minimum information code, consisting either of “dead” code (code we may avoid evaluating), or of code whose “useful part” is constant. Both kinds of code may be removed, speeding-up the evaluation in this way: we introduce an algorithm for doing it. We prove the correctness...
We present a new type system for the Lambda Calculus of Objects [16], based on matching. The new system retains the property of type safety of the original system, while using implicit match-bounded quantification over type variables instead of implicit quantification over row schemes (as in [16]) to capture Mytype polymorphic types for methods. Type soundness for the new system is proved as a direct...
We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive characterizations of type containment and type equality via simulation and bisimulation, respectively. The main novelty of the axiomatization is the fixpoint rule (or coinduction principle), which has the form...
Usually types of PCF are interpreted as cpos and terms as continuous functions. It is then the case that non-termination of a closed term of ground type corresponds to the interpretation being bottom; we say that the semantics is adequate. We shall here present an axiomatic approach to adequacy for PCF in the sense that we will introduce categorical axioms enabling an adequate semantics to be given...
We introduce a technique based on logical relations, which, given two models M and N of a simply typed lambda-calculus L, allows us to construct a model M/N whose L-theory is a superset of both Th(M) and Th(N).
Several proof-assistants rely on the very formal basis of Pure Type Systems (PTS). However, some practical issues raised by the development of large proofs lead to add other features to actual implementations for handling namespace management, for developing reusable proof libraries and for separate verification of distinct parts of large proofs. Unfortunately, few theoretical basis are given for...
In this paper we introduce an algorithm for detecting strictness information in typed functional programs. Our algorithm is based on a type inference system which allows to exploit the type structure of the language for the investigation of program properties. The detection of strictness information can be performed in a complete way, by reducing it to the solution of a set of constraints involving...
Although the use of expansionary η-rewrite has become increasingly common in recent years, one area where ν-contractions have until now remained the only possibility is in the more powerful type theories of the λ-cube. This paper rectifies this situation by applying η-expansions to the Calculus of Constructions — we discuss some of the difficulties posed by the presence of dependent types, prove that...
We study the problem of local and asynchronous computation in the context of multiplicative exponential linear logic (MELL) proof nets. The main novelty is in a complete set of rewriting rules for cut-elimination in presence of weakening (which requires garbage collection). The proposed reduction system is strongly normalizing and confluent.
Cyclic sharing (cyclic graph rewriting) has been used as a practical technique for implementing recursive computation efficiently. To capture its semantic nature, we introduce categorical models for lambda calculi with cyclic sharing (cyclic lambda graphs), using notions of computation by Moggi/Power and Robinson and traced monoidal categories by Joyal, Street and Verity. The former is used...
We present a game model for classical PCF, a finite version of PCF extended by a catch/throw mechanism. This model is build from E-dialogues, a kind of two-players game defined by Lorenzen. In the E-dialogues for classical PCF, the strategies of the first player are isomorphic to the Bhöhm trees of the language. We define an interaction in E-dialogues and show that it models the weak-head reduction...
Two variations of the intersection type assignment system are studied in connection with Böhm-trees. One is the intersection type assignment system with a non-standard subtype relation, by means of which we characterize whereabouts of D in Böhm-trees. The other is a refinement of the intersection type assignment system whose restricted typability is shown to coincide with finiteness of Böhm-trees.
Coinductive (applicative) characterizations of various observational congruences which arise in the semantics of λ-calculus, for various reduction strategies, are discussed. Two semantic techniques for establishing the coincidence of the applicative and the contextual equivalences are analyzed. The first is based on intersection types, the second is based on a mixed induction-coinduction principle...
We consider the lambda definability problem over an arbitrary free algebra. There is a natural notion of primitive recursive function in such algebras and at the same time a natural notion of a lambda definable function. We shown that the question: ”For a given free algebra and a primitive recursive function within this algebra decide whether this function is lambda definable” is undecidable if the...
A rewrite sequence is said to be outermost-fair if every outermost redex occurrence is eventually eliminated. O'Donnell has shown that outermost-fair rewriting is normalising for almost orthogonal first-order term rewriting systems. In this paper we extend this result to the higher-order case.
We extend the multiplicative fragment of linear logic with a non-commutative connective (called before), which, roughly speaking, corresponds to sequential composition. This lead us to a calculus where the conclusion of a proof is a Partially Ordered MultiSET of formulae. We firstly examine coherence semantics, where we introduce the before connective, and ordered products of formulae. Secondly...
This paper describes a computational reflection mechanism for the calculus of constructions. In this framework it is possible to encode functions that operate on syntactic representations on the meta-level and to verify semantic relations between the object-level denotations of the source and the target of meta-functions. Moreover, it is shown how computational reflection can easily be integrated...
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.