Next: Warsaw
Up: Cooperating sites
Previous: Toulouse


Udine

The Formal Methods and Logics of Computation (FMLC) group at the Department of Mathematics and Computer Science of the University of Udine, has been involved in all four previous TYPES projects founded by the EU. The FMLC group has international reputation in type theory, lambda calculi, Logical Frameworks, Non Wellfounded Set Theory, Coinductive and Coalgebraic methods, and Exact Real Numbers computation. Recent work has focussed on the syntax and semantics of programming languages and the algebraic, categorical, logical, and geometric models which support the verification and analysis of programs, as well as the areas of Game Semantics and stepwise data refinement.

The group plans to contribute to the following objectives of this proposal.

Correctness of Computer Systems

Computer arithmetic through our ongoing work on exact real computation using coinductive types. Programming language features: we have formalized in Coq an object-oriented language with side effects, and proved some important properties. We plan to continue this line of research, by developing certified tools (e.g., interpreters) for this kind of languages. Another line of research on this issue is the use of coinductive principles for reasoning on object oriented languages.

Foundational research

Logical Frameworks: we are active in the area of Higher Order Abstract Syntax and binding, especially with regard to structural induction and recursion over abstract syntax. We are also working on foundational results unifying inductive and coinductive definitions, and covering many naturally occurring examples. We plan to investigate more liberal principles for such definitions.

The senior members of the group are

Udine homepage

Bengt Nordström 2005-09-22