The paper presents a calculus and a modal semantic for the logic of intersection types of lambda-calculus already studied by Barendregt, Dezani and others and proves the completeness theorem for this logic as well as the cut elimination theorem, the finite model property and a decidability algorithm.
A binary modal logic for the intersection types of lambdacalculus.
VIALE, Matteo
2003-01-01
Abstract
The paper presents a calculus and a modal semantic for the logic of intersection types of lambda-calculus already studied by Barendregt, Dezani and others and proves the completeness theorem for this logic as well as the cut elimination theorem, the finite model property and a decidability algorithm.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
