Common Foundations of Functional and Logic Programming

GENTZEN - 7232

Work Area: Logics and Logic Programming

Keywords logic, logic programming, functional programming

Start Date: 1 November 92 / Duration: 36 months / Status: running

[ participants / contact ]

Abstract Logics, logic programming and theories of computation are viewed as different aspects of a unified theory still to be constructed, and whose relevant byproducts would be prototypes. The work builds on the results of the CFFLP (3230) working group.


Different methodologies and new programming techniques (such as object-oriented programming and complexity evaluations) will be analysed and their common foundations examined.

Each methodology is connected to well-established lines of research lines, namely programs as proofs, programs as algebraic and recursive specifications, and programs as untyped x-terms. The principal problems are in realisation and integration.

The tools involved are: proof theory, lambda calculus and combinatory logic, type theory, universal algebra, horn logic.


Informal workshops in each of the main lines of research.

Three general meetings: the first one to be held in 1993 in conjunction with the "Extensions of Logic Programming" Conference, the second one to be held in Marseille at the Institute de Mathématiques Discrétes (1994), and the third in Rome (1995).


In the short term, exploitation of the research is likely to arise through the improvement of existing prototypes developed in some sites of the working group and the realisation of programming language tools (eg type checkers, reduction machines) partly supporting functional and logic programming styles.

In the medium term, basic tools implementing foundational styles (eg cut eliminator, proof extractor, equation solver, game player) should be realised.

In the long term, according to the main streams of common foundations for functional and logic programming, tools and environments supporting full integration of both styles of programming and possibly others should be built.


Università di Roma La Sapienza - I
Dipartimento de Scienze dell'Informazione
via Salaria 116
I - 00198 ROMA


Ludwig Maximilians Universität München - D
Universität Kaiserslautern - D
Universität Tübingen - D
Université de Pari-Sud - F
National Technical University of Athens - GR
University College Swansea - UK
University of St. Andrews - UK


Prof. C. Böhm
tel +39/6 8845235
fax +39/6 8841964

LTR synopses home page LTR work area index LTR acronym index LTR number index LTR Working Groups index
All synopses home page all acronyms index all numbers index

GENTZEN - 7232, August 1994

please address enquiries to the ESPRIT Information Desk

html version of synopsis by Nick Cook