Research activity in 1994
The research activity of the theory group has mainly achieved the followng
results:
- the study of lambda terms representing proofs in formal systems of
constructing mathematics, and their use and optimization in automatic program
syntesis
- the developmento of an algebraic approach to recursive types interpretation
in functional and object-oriented programming
- study of the notion of type in programming languages and its connection with
the notions of theorem and demonstration in logics
- study of type inference strategies and the use of the notion of type in the
demonstration of program properties, like strictness properties
- the type systems with inheritance for modelling of object-oriented
programming concepts
- analisis of the main synthactic and semantic properties of some polymorphic
type systems containing interesting operators for type formation (like
exponentiation, universal and existencial quantification, intersection, union,
recursion)
- definition and study of the semantics of call-by-value lambda calculus using
three standard approach for programming language semantics, i.e. the
operational, denotational and logical approach.
- charaterisation of proof-theoritic type operators, which express the notion
of functional dependence between algorithms using the notion of derivability in
non classical logics, like relevance and linear logic.
