n 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.
Extracting information from intermediate semiconstructive HA-systems - extended abstract / M. Ferrari, C. Fiorentini, P. Miglioli. - In: MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE. - ISSN 0960-1295. - 11:4(2001), pp. 589-596. [10.1017/S0960129501003358]
Extracting information from intermediate semiconstructive HA-systems - extended abstract
C. Fiorentini;
2001
Abstract
n 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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
2001_mscs.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
552.78 kB
Formato
Adobe PDF
|
552.78 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
