Output details
11 - Computer Science and Informatics
Imperial College London
Return to search
Output 0 of 0 in the submission
Article title
Computation with classical sequents
Type
D - Journal article
Title of journal
Mathematical Structures in Computer Science
Article number
-
Volume number
18
Issue number
3
First page of article
555
ISSN of journal
0960-1295
Year of publication
2008
URL
-
Number of additional authors
1
Additional information
<11> The paper presents X which provides a Curry-Howard isomorphism for Gentzen's sequent logic LK. We embedded the lambda-calculus, lambda-x, lambda-mu, and Curien and Herbelin's LMMT into X, and show that X gives a fine-grained reduction engine for all. This paper allows for the study of parameter and context call with explicit substitution, and has led to the study of the relation between logic and the pi-calculus (van Bakel-Vigliotti CONCUR '09), semantics of sequent calculi and lambda-mu (van Bakel APAL'10), two PhD theses, on theory and on the implementation of a reduction and type assignment tool.
Interdisciplinary
-
Cross-referral requested
-
Research group
E - Programming Languages and Systems
Citation count
4
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
