Mathematical Structures in Computer Science


Special Issue: Modalities in Type Theory

Extracting information from intermediate semiconstructive HA-systems – extended abstract 1


MAURO FERRARI a1, CAMILLO FIORENTINI a1 and PIERANGELO MIGLIOLI a1
a1 Università degli Studi di Milano, Dipartimento di Scienze dell'Informazione, via Comelico 39, 20135 Milano, Italy

Abstract

In this abstract we will describe research in progress on the problem of extracting information from proofs. Here we will concentrate our attention on semiconstructive calculi, which is a kind of calculus that is of interest in the framework of program synthesis and formal verification. We will discuss the notion of uniformly semiconstructive calculus, introduce our information extraction mechanism and apply it to two calculi extending Intuitionistic Arithmetic.

(Received October 1 1999)
(Revised May 15 2000)



Footnotes

1 The full version of this paper is available at http://homes.dsi.unimi.it/˜ferram