University of Udine

Topics

  • Theory  of Logical Frameworks and Case Studies in Formal Verification
  • Pre-logical Relations and Step-wise Data Refinement
  • Coalgebraic analysis of Coinduction and Coinductive Types
  • Game Semantics for Lambda Calcului
  • Exact Real NumberComputation

    • Team

    Theory  of Logical Frameworks and Case Studies in Formal Verification

        The Udine group has studied various topics in the theory and practice of Logical Frameworks based on (impredicative) Higher Order Type Theories,  such as CC(Co)Ind.  In particular, the group has continued  to explore the possibility of encoding  program logics and process calculi utilizing  higher order abstract syntax (HOAS)  presentations of systems, often in natural deduction style.  As it is well known, HOAS presentations are useful in that they allow to delegate to the metalanguage much of the machinery related to the use of binding operators. When, moreover, these are in natural deduction style, one can  capitalize furthermore on the structure of the metalanguage, and treat naturally  on a par basic judgements, hypotheses and rules.
        However, many subtle issues have to be dealt with in connection with program variables and proof rules in order to define  faithful HOAS  encodings. To this end, the Udine group has developed a general methodology, based on a  comprehensive repertoire of encoding techniques.
        A wide range of case studies involving program logics, calculi, and systems has been investigated.  In particular, the Udine group has considered natural operational semantics,  Hoare's logic, dynamic logic, modal logics, mu-calculus , process calculi [1,2,3,4]. This investigation has culminated  with the extended case study of the formal metathoery of pi-calculus [5], as discussed by Milner, Parrow, and Walker.  In this work, heavy use of coinductive types has been made in order to encode observational equivalences.
        When dealing with higher order abstract syntax presentations, formal proofs of  metatheoretical properties of the system can be problematic. This is due to the difficulty of reasoning inductively on the syntax of the object language, which derives from the fact that object variables coincide with metalanguage variables.  The case-study on the pi-calculus has shown, however, that this approach is viable,  at the price of introducing a few natural axioms, whose consistency can be intuitively justified by a direct application of the reflection principle.
        All case studies have been implemented in Coq, the proof development environment for the (Co)Inductive Type Theory CC(Co)Ind.

    Pre-logical Relations and Step-wise Data Refinement


       The Udine group has focused on the foundations of type systems for ``delegation-based'' Object Oriented programming languages. In these languages objects are defined directly using an already existing object as a prototype. The only operations on objects are object extension and object override. Adding or overriding an object produces a new object which inherits all the properties of the original object.  In particular, the Udine group (and especially L.Liquori) has analyzed various type systems  for various object calculi based on the Lambda Calculus of Objects,  introduced by  Fisher,  Honsell and Mitchell (LICS93), and the Theory of Objects introduced by Abadi  and Cardelli (Springer 1996), see [6,7,8].  These languages feature a simple mechanism of inheritance, dynamic lookup, method specialization  (i.e. the possibility to specialize the types of the inherited methods). The type systems are essentailly intended to catch the ``message-not-understood'' run-time error.
        The possibility of typing soundly lambda calculi with primitives for manipualting objects, where objects might extend themselves upon receiving a message, has been analyzed in [9].  This feature  had never been considered before.

     

    Coalgebraic Analysis of Coinduction and Coinductive Types 
     
       Marina Lenisa has explored the set-thoretic, categorical, and logical foundations, as well as the applicability of the final semantics paradigm, introduced by P.Aczel, and further developed by J.Rutten and D.Turi. The interest of final semantics lies in the fact that it provides a principled, uniform explanation of coinduction principles . Lenisa has shown that final semantics is widely applicable,and she has discussed in detail final semantics for process algebra languages,  higher order imperative concurrent languages,  functional languages, and  calculi for mobile processes, [11]. Particular attention has been put in the possibility of defining final semantics in an elementary setting such as that of non-wellfounded sets.
       An interesting spin-off of this research in the logical foundations of coinduction principles, was the introduction of a logical system, inspired by work of Coquand, for establishing bisimulation equivalences over regular circular objects. These objects are definable using a typed language, whose coinductive types involve disjoint sum, cartesian product, and finite powerset constructors.

    [10] Marina Lenisa A Coinductive Logical System for Bisimulation Equivalence of
    Circular Objects,
    Technical report Udine University, April 1998.
    We introduce a coinductive logical system a' la Gentzen for establishing bisimulation equivalences on circular  objects, inspired by work of Coquand. For describing such infinite regular objects, we utilize a typed language, whose coinductive types involve disjoint sum, cartesian product, and finite powerset constructors. This system is shown to be complete with respect to a maximal fixed point semantics. It is shown to be complete also with respect to an equivalent final semantics. In this latter semantics, terms are viewed as points of a coalgebra for a suitable endofunctor on the category Set* of  non-wellfounded sets. This system subsumes an axiomatization of regular processes, alternative to the classical one given by Milner.

    [5] Furio Honsell, Marino Miculan, Ivan Scagnetto.
    $\pi$-calculus in (Co)Inductive Type Theory
    Technical  Report, University of Udine, August 1998
    Abstract:
     We present a large and we think also significant case-study in  computer assisted formal reasoning.  We start by giving a  higher order abstract syntax encoding of $\pi$-calculus in the  higher-order inductive/coinductive type theories CIC and CC(Co)Ind.  This  encoding gives rise to a full-fledged proof editor/proof assistant  for the $\pi$-calculus, once we embed it in Coq, an interactive proof-development environment for CC(Co)Ind.  Using this computerized  assistant we prove formally a substantial chapter of the theory of  strong late bisimilarity, which amounts essentially to Section 2 of A calculus of mobile processes by Milner,  Parrow, and Walker.  This task is greatly simplified by the use of  higher order syntax. In fact, not only we can delegate conveniently to the metalanguage $\alpha$-conversion and substitution, but,  introducing a suitable axiomatization of the theory of contexts, we  can accommodate also the machinery for generating new names.  The axiomatization we introduce is quite general and should be easily  portable to other formalizations based on higher order syntax.  The use of coinductive types and corresponding tactics allows to give alternative, and possibly more natural, proofs of many properties of  strong late bisimilarity, w.r.t. those originally given by Milner,  Parrow, and Walker.
     

    Game Semantics for Lambda Calculus

       The Udine group has investigated the possibility of defining non-initial solutions of recursive equations in the category of games, introduced by Abramsky, Jagadeesan, and Malacaria. Moreover they have shown that, as far as untyped lambda calculus, game semantics is more rigid than continuous semantics, in that all extensional game models induce the same lambda theory [16]. This is not the case in CPO.
        Di Gianantonio and Franco have studied also the possibility of giving a finitary logical description of games semantics. As a case study, the finitary description of a game semantic model for the lambda calculus is presented in full, [17].

    [16] Pietro Di Gianantonio, Gianluca Franco, Furio Honsell
    Game semantics for untyped lambda\beta\eta-calculus
    Technical report - University of Udine August 1998
    Abstract:
    We study extensional models of the untyped lambda calculus in the setting of game semantics. In particular, we show that, somewhat unexpectedly and contrary to what happens in ordinary categories of domains, all reflexive objects in the category of games G, introduced by Abramsky, Jagadeesan and Malacaria, induce the same lambda-theory. This is H*, the maximal theory induced already by the classical CPO model D_{\infty}, introduced by Scott in 1969. This results indicates that the current notion of game carries a very specific bias towards head reduction.

    [17] Pietro Di Gianantonio, Gianluca Franco
    A type assignment system for game semantics
    To appear in Proc. ICTCS'98.  World Scientific.
    Abstract: In this paper an alternative description of the game semantics for the untyped lambda calculus is given. More precisely, we introduce a finitary formal description of lambda terms. This description turns out to be equivalent to a particular game denotational semantics of the lambda calculus
     

    Exact Real Number Computation

        Pietro Di Gianantonio has continued his investigation of the foundations of computability on exact real numbers. In particular he has considered the problem whether the use of parallel operators is necessary in calculi having real numbers as an abstract data type [18].
           Moreover Ciaffaglione, Di Gianantonio and Honsell have explored the possibility of proving formally, using the proof environment for impredicative type theory Coq, basic results in the theory of exact real numbers. The aim is to introduce a structure for the exact reals and to prove foramlyy that that it adesatisfies all the axioms for the real numbers. This wil provide an implementation, in Coq, of the constructive reals, implementation that is still missing.
    Reals are represented as equivalence classes of streams of digits under a coinductively defined equivalence relation. In particular, they have formally proved, all the axioms for the order relation and various properties of addition. have explored the possibility of proving formally, using the proof environment for impredicative type theory Coq, basic results in the theory of exact real numbers. They have represented reals as equivalence classes of streams of binary digits under a coinductively defined equivalence relation. This equivalence is the one determined by the binary notation introduced by Di Gianantonio which uses the Golden Ratio as base. In particular, they have formally proved various properties of the algorithm defined by Di Gianantonio for addition.

    [18] Pietro Di Gianantonio
    An abstract data type for real numbers.
    Theoretical Computer Science, 221:295-326, 1999.
    Abstract:
    We present a calculus having real numbers as a basic data type. The calculus is defined by its denotational semantics. We prove the universality of the calculus. We show how the definition of an operational semantics is problematic. We discuss this problem and present a possible solution.
     

    MSCS 9(4) Special Issue on Lambda-Calculus and Logic in Honour F.Honsell, M.Lenisa. Semantical analysiss of perpetual strategies in lambda-calculus, Theoretical Computer Science 212, 1999, 183--209. F.Honsell, M.Lenisa. Coinductive Characterizations of Applicative Structures, Math. Struct. in Comp. Science 9, 1999. M.Lenisa. A Complete Coinductive Logical System for Bisimulation Equivalence on Circular Objects, FoSSaCS'99 (ETAPS) Conf. Proc., W.Thomas ed., Springer LNCS 1578, 1999, 243--257. M.Lenisa. From Set-theoretic Coinduction to Coalgebraic Coinduction: some results, some problems, Coalgebraic Methods in Computer Science'99 Conf. Proc., ENTCS 19, 1999, 1--22. S.Abramsky, M.Lenisa. Fully Complete Models for ML Polymorphic Types, Technical Report ECS-LFCS-99-414, 39 pages.