LFCS
2016
Springer
8 years 7 months ago
2016
Springer
We investigate (co-)induction in Classical Logic under the propositions-as-types paradigm, considering propositional, second-order, and (co-)inductive types. Specifically, we intr...
LFCS
2016
Springer
8 years 7 months ago
2016
Springer
In contrast to most kinds of computability studied in mathematical logic, feedback computability has a non-degenerate notion of parallelism. Here we study parallelism for the most...
LFCS
2016
Springer
8 years 7 months ago
2016
Springer
We generalize the adjoint logics of Benton and Wadler (1996) and Reed (2009) to allow multiple different adjunctions between the same categories. This provides insight into the str...
LFCS
2016
Springer
8 years 7 months ago
2016
Springer
LFCS
2016
Springer
8 years 7 months ago
2016
Springer
Abstract. We present a soundness theorem for a dependent type theory with context conith respect to an indexed category of (finite, abstract) simplical complexes. The point of int...