LPCIC

Logic Programming for the Calculus of Inductive Construction

Description

Members

System

Description

The aim of the project is the study of the type checking, type inference and unification algorithms for the Calculus of Inductive Construction in the λ-prolog language.

It is a cooperation between the Dipartimento di Informatica - Scienza e Ingegneria of the University of Bologna, INRIA Sophia Antipolis and INRIA Saclay.

! TU Wien