Decomposing typed lambda calculus into
a couple of categorical programming languages
In
Proc. 6th International Conference on Category Theory and Computer Science
(CTCS'95), Springer LNCS 953 (1995) 200-219
Abstract
We give two categorical programming languages
with variable arrows and associated abstraction/reduction
mechanisms, which extend the possibility of categorical programming
[1,2] in practice. These languages are complementary to
each other -- one of them provides a first-order programming style
whereas the other does higher-order -- and are ``children'' of the
simply typed lambda calculus in the sense
that we can decompose typed lambda calculus into them and, conversely,
the combination of them is equivalent to typed lambda calculus.
This decomposition is a consequence of a semantic analysis on typed
lambda calculus due to C. Hermida and B. Jacobs [3].
Pointers to Related Work
- [1]
T. Hagino,
A Categorical Programming Language.
PhD thesis ECS-LFCS-87-38, University of Edinburgh (1987).
- [2] J.R.B. Cockett and T. Fukushima,
About Charity.
Technical report 92/480/18, University of Calgary (1992).
- [3] C. Hermida and
B. Jacobs,
Fibrations with indeterminates: contextual and functional
completeness for polymorphic lambda calculi.
Mathematical Structures in Computer Science
5(4) (1995) 501-531.
- A.J. Power and
H. Thielecke,
Environments, continuation semantics and indexed categories.
In Proc. TACS'97, Springer LNCS 1281 (1997) 391-414.
- A.J. Power and
H. Thielecke,
Closed Freyd- and kappa-categories.
In Proc. ICALP'99, Springer LNCS 1644 (1999).
Back to Hassei's
Research Page / Home Page