# Formalizing the left-chiastic simply-typed lambda calculus, or: What I did last summer

### Wren Thornton

## Abstract

A couple years ago, in order to handle scrambling in Japanese, I introduced a new calculus for the semantic side of CCG derivations. This simple calculus is easy to describe and it can also be used to formalize keyword-arguments in programming languages, to justify notational shorthands in category theory, and numerous other things I keep stumbling upon. The calculus ties together a number of disparate threads in theoretical linguistics, type theory, logic, and category theory; and seems therefore worthy of future study. But one nagging question is: is it a nice place to do work? Does the calculus have the properties we usually desire from computational formalisms, like confluence and strong normalization?

This summer I worked on answering these questions. Some have been answered in the affirmative. Others remain open, due to limitations in our usual techniques for solving themâ€” and perhaps due to limitations in our understanding of the phenomena in question. This talk relays some of that exploration.