Fundamenta Informaticae - Volume 77, issue 4

Article Type: Other

Citation: Fundamenta Informaticae, vol. 77, no. 4, pp. i-i, 2007

Authors: Coquand, Thierry

Article Type: Research Article

Abstract: We present a variation of Hindley's completeness theorem for simply typed λ-calculus. It is based on a Kripke semantics where the worlds are contexts, called context-semantics. This variation was obtained indirectly by simplifying an analysis of a fragment of polymorphic λ-calculus [2]. We relate in this way works done in proof theory [4,14] with a fundamental result in λ-calculus.

Citation: Fundamenta Informaticae, vol. 77, no. 4, pp. 293-301, 2007

Authors: Felty, Amy P.

Article Type: Research Article

Abstract: Proof-carrying code provides amechanismfor insuring that a host, or code consumer, can safely run code delivered by a code producer. The host specifies a safety policy as a set of axioms and inference rules. In addition to a compiled program, the code producer delivers a formal proof of safety expressed in terms of those rules that can be easily checked. Foundational proof-carrying code (FPCC) provides increased security and greater flexibility in the construction of proofs of …safety. Proofs of safety are constructed from the smallest possible set of axioms and inference rules. For example, typing rules are not included. In our semantic approach to FPCC, we encode a semantics of types from first principles and the typing rules are proved as lemmas. In addition, we start from a semantic definition of machine instructions and safety is defined directly from this semantics. Since FPCC starts from basic axioms and low-level definitions, it is necessary to build up a library of lemmas and definitions so that reasoning about particular programs can be carried out at a higher level, and ideally, also be automated. We describe a high-level organization that involves Hoarestyle reasoning about machine code programs. This organization is presented using two running examples. The examples, as well as illustrating the above mentioned approach to organizing proofs, is designed to provide a tutorial introduction to a variety of facets of our FPCC approach. For example, it illustrates how to prove safety of programs that traverse input data structures as well as allocate new ones. Show more

Citation: Fundamenta Informaticae, vol. 77, no. 4, pp. 303-330, 2007

Authors: Hayashi, Susumu

Article Type: Research Article

Abstract: Proof animation is a way of executing proofs to find errors in the formalization of proofs. It is intended to be "testing in proof engineering". Although the realizability interpretation as well as the functional interpretation based on limit-computations were introduced as means for proof animation, they were unrealistic as an architectural basis for actual proof animation tools. We have found a game theoretic semantics corresponding to these interpretations, which is likely to be the right …architectural basis for proof animation. Show more

Keywords: Game semantics, Computations in Classical Logic, Learning theory

Citation: Fundamenta Informaticae, vol. 77, no. 4, pp. 331-343, 2007

Authors: Abel, Andreas | Coquand, Thierry

Article Type: Research Article

Abstract: Martin-Löf's Logical Framework is extended by strong Σ-types and presented via judgmental equality with rules for extensionality and surjective pairing. Soundness of the framework rules is proven via a generic PER model on untyped terms. An algorithmic version of the framework is given through an untyped βη-equality test and a bidirectional type checking algorithm. Completeness is proven by instantiating the PER model with η-equality on β-normal forms, which is shown equivalent to the algorithmic …equality. Show more

Citation: Fundamenta Informaticae, vol. 77, no. 4, pp. 345-395, 2007

Authors: Ahmed, Amal | Fluet, Matthew | Morrisett, Greg

Article Type: Research Article

Abstract: We present a simple, but expressive type system that supports strong updates – updating a memory cell to hold values of unrelated types at different points in time. Our formulation is based upon a standard linear lambda calculus and, as a result, enjoys a simple semantic interpretation for types that is closely related to models for spatial logics. The typing interpretation is strong enough that, in spite of the fact that our core programming language supports …shared, mutable references and cyclic graphs, every well-typed program terminates. We then consider extensions needed to model ML-style references, where the capability to access a reference cell is unrestricted, but strong updates are disallowed. Our extensions include a thaw primitive for re-gaining the capability to perform strong updates on unrestricted references. The thaw primitive is closely related to other mechanisms that support strong updates, such as CQUAL's restrict. Show more

Citation: Fundamenta Informaticae, vol. 77, no. 4, pp. 397-449, 2007

Authors: Damiani, Ferruccio

Article Type: Research Article

Abstract: Let ⊢ be an intersection type system. We say that a term is ⊢-simple (or just simple when the system ⊢ is clear from the context) if system ⊢ can prove that it has a simple type. In this paper we propose new typing rules and algorithms that are able to type (with rank 2 intersection types) recursive definitions that are not simple. Typing rules for assigning intersection types to (nonsimple) recursive definitions have been already proposed in the …literature. However, at the best of our knowledge, previous algorithms for typing recursive definitions in the presence of intersection types allow only simple recursive definitions to be typed. The rules and algorithms proposed in this paper are also able to type interesting examples of polymorphic recursion (i.e., recursive definitions rec {x=e} where different occurrences of x in e are used with different types). Moreover, the underlying techniques do not depend on particulars of rank 2 intersection, so they can be applied to other type systems. Show more

Keywords: Type inference, Principal typings, Polymorphic recursion

Citation: Fundamenta Informaticae, vol. 77, no. 4, pp. 451-488, 2007

Authors: David, René | Nour, Karim

Article Type: Research Article

Abstract: We give arithmetical proofs of the strong normalization of two symmetric λ-calculi corresponding to classical logic. The first one is the λ¯μμ˜-calculus introduced by Curien & Herbelin. It is derived via the Curry-Howard correspondence from Gentzen's classical sequent calculus LK in order to have a symmetry on one side between "program" and "context" and on other side between "call-by-name" and "callby-value". The second one is the symmetric λμ-calculus. It is the λμ-calculus introduced …by Parigot in which the reduction rule μ', which is the symmetric of μ, is added. These results were already known but the previous proofs use candidates of reducibility where the interpretation of a type is defined as the fix point of some increasing operator and thus, are highly non arithmetical. Show more

Citation: Fundamenta Informaticae, vol. 77, no. 4, pp. 489-510, 2007

Authors: Laird, James D.

Article Type: Research Article

Abstract: We use a denotational semantics to show that every term in SPCF (a typed functional language with simple non-local control operators) is contextually equivalent to one which is typable in an affine typing system. Nested function calls and recursive definitions are not affinely typable, and so our result entails that they can be eliminated from SPCF without losing expressiveness. Our proof is based on the observation of Longley that every type of SPCF is …a retract of a first-order type. We describe retractions of this kind in bistable biorder models of SPCF which are definable in the affine fragment. This allows us to transform an arbitrary SPCF term into an affine one by mapping it to a first-order term, obtaining an (affine) "normal form", and then projecting back to the original type. We show the flexibility of our approach by considering two variants of SPCF, a finitary, call-byname version and a call-by-value version over the natural numbers. In the infinitary case, (in which we establish in addition that all instances of recursive definition may be replaced with iteration) our proof is based on an analysis of the relationship between SPCF definable functions and strategies for computing them sequentially. Show more

Citation: Fundamenta Informaticae, vol. 77, no. 4, pp. 511-531, 2007