The Udine group has studied various issues in the theory and practice of Logical Frameworks based on Constructive Type Theories. In particular Honsell, Miculan and Lenisa have addressed the problem of representing faithfully process algebras, such as CCS and pi-calculus, in coinductive theories of types such as Gimenez CCco(ind), and they have developed proof editors for such systems in Coq. Di Gianantonio and Honsell have studied the possibility of proving formally in Coq basic results in the theory of exact computation on reals numbers. Di Gianantonio has studied also the theory of exact real number computation. He has introduced a domain of approximations and an abstract data type for the real numbers, considering also the problem of implementing such an abstract data type. In particular, he has shown (ICALP 97) that, for several representations of real numbers, it is necessary to use programming languages having parallel operators in order to have a faithful implementaion. Liquori has studied theories of typed lambda calculi, with primitives for manipulating objects. Cabroni has studied the problem of representing Hoare Logics in Coq. Franco has studied issues in game semantics.