Name
Title | ||
|---|---|---|
Confluence For Classical Logic Through The Distinction Between Values And Computations |
Abstract | ||
|---|---|---|
We apply an idea originated in the theory of programming languages-monadicmeta-language with a distinction between values and computations-in the design of a calculus of cut-elimination for classical logic. The cut-elimination calculus we obtain comprehends the call-by-name and call-by-value fragments of Curien-Herbelin's (lambda) over bar mu(mu) over tilde -calculus without losing confluence, and is based on a distinction of "modes" in the proof expressions and "mode" annotations in types. Modes resemble colors and polarities, but are quite different: we give meaning to them in terms of a monadic meta-language where the distinction between values and computations is fully explored. This metalanguage is a refinement of the classical monadic language previously introduced by the authors, and is also developed in the paper. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.4204/EPTCS.164.5 | ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE |
Field | DocType | Issue |
Discrete mathematics,Expression (mathematics),Confluence,Classical logic,Monadic predicate calculus,Monad (functional programming),Calculus,Mathematics,Computation | Journal | 164 |
ISSN | Citations | PageRank |
2075-2180 | 0 | 0.34 |
References | Authors | |
11 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| José Espírito Santo | 1 | 62 | 10.79 |
| Ralph Matthes | 2 | 201 | 21.67 |
| Koji Nakazawa | 3 | 36 | 6.92 |
| Luis Pinto | 4 | 69 | 12.04 |