Conservative extensions of the λ-calculus for the computational interpretation of sequent calculus
This thesis offers a study of the Curry-Howard correspondence for a certain fragment (the canonical fragment) of sequent calculus based on an investigation of the relationship between cut elimination in that fragment and normalisation. The output of this study may be summarised in a new assignment T...
| Main Author: | |
|---|---|
| Other Authors: | |
| Published: |
University of Edinburgh
2002
|
| Subjects: | |
| Online Access: | https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.561802 |