1991-1992

Abstract
Intuitionistic logic nowdays is usually considered in the context of formulas as types. This analogy is inspired by theorem of Curry (1968) that in pure implicative logic proofs one-to-one correspond to strictly typed lambda-terms; formulas to their types.
Lecture is devoted to analysis of real analogies of proofs (in predicate calculus) and programs (in language of functional programming).
Abstract Kleene-like realizability is considered and Shanin-like algorithm of constructive deciphering. Sources of ghost values and passive formulas which have no images in a working program are investigated.
Finite type extension of intuitionistic logic and intuitionistic logic with partially ordered quantifiers are condsidered. Linear part of intuitionistic logic and modular constraining of intuitionistic logic are considered in comparison with introduced models and extracted programs.

conf.n.8

( Pagina di benvenuto

Indice 1991-92

Indice per a.a.

Indice conferenziere

Indice per nomi )

martedì 10/3/1992, ore 17, aula E

Gianfranco Mascari

Semantiche della logica lineare: rappresentazioni di gruppi e C*-algebre

conf.n.9

( Pagina di benvenuto

martedì 24/3/1992, ore 17, aula E

Luca Aceto
(Lavoro in collaborazione con Bard Bloom (Cornell University) e Frits Vaandrager (Ecole des Mines, CMA))

Turning SOS rules into equations
o "Come Convertire una Semantica Operazionale in una Equazionale"

Abstract
La semantica operazionale di molte algebre di processi è data nello stile della Semantica Operazionale Strutturata (SOS) di Plotkin. Queste semantiche operazionali possono essere classificate a seconda del tipo di regole inferenziali che utilizzano. Uno dei formati di regole più generali è il formato GSOS proposto da Bloom, Istrail e Meyer.
In questo seminario, presenterò una procedura per convertire una qualsiasi semantica operazionale in stile GSOS in un sistema finito di assiomi equazionali (eccetto il possibile uso di una equazione condizionale infinitaria), che caratterizza completamente la bisimulazione tra processi.

conf.n.10

( Pagina di benvenuto

martedì 7/4/1992, ore 17, aula E

Marco Grandis

Algebra omotopica: un'impostazione categoriale bidimensionale

conf.n.11

( Pagina di benvenuto

lunedì 13/4/1992, ore 17, aula G

Silvia Gilezan

Abitabilità dei tipi intersezione intersection types and logic

conf.n.12

( Pagina di benvenuto

martedì 5/5/1992, ore 16, aula E

Rocco De Nicola

Algebre di processi e logiche modali

conf.n.13

( Pagina di benvenuto

martedì 5/5/1992, ore 17, aula E

Alberto Pettorossi

Eliminazione di variabili non necessarie in programmazione logica
cioè: come comporre e tuplare relazioni in modo efficiente

Abstract
Quando si scrivono programmi logici si usano spesso variabili intermedie che non occorrono nella relazione da calcolare (cioè nel predicato di testa) o variabili che occorrono più di una volta nel corpo della clausola. Per esempio, nella clausola C₁: p(in,out) <- q(in,v₁),r(v₁,out) la variabile v₁ è intermedia, mentre nella clausola C₂: p(in,out) <- q(in,out),s(in) la variabile "in" occorre due volte nel corpo.
Presenteremo una tecnica che elimina l'inefficienza dovuta all'occorrenza di queste variabili, chiamate collettivamente variabili non necessarie. Nel caso della calusola C₁ l'eliminazione di variabili non necessarie corrisponde alla composizione di relazioni, mentre nel caso della clausola C₂ corrisponde al tupling di relazioni.