It is a common refrain here at Carnegie Mellon University that structural operational semantics (SOS) is the best form of dynamics, and that contextual dynamics (“Indiana-style semantics”) do not combat the bureaucratic tendency in the way that they are usually claimed to do. This is true in one formulation of contextual dynamics, but I would like to demonstrate a more fine-grained approach that is an improvement on both SOS and standard contextual dynamics.

*Dialectical materialism*, far from being merely the definitive theory of political and historical movement, also serves as the guiding light for the progressive mathematician in its manifestation as the science of adjoint functors in category theory.

As Lawvere stated in his influential note *Quantifiers and Sheaves*, the essential move in mathematics is to identify the principal contradictions of a theory in the form of pairs of adjoint functors, and to “weaponize” them as slogans to drive the further development (and generalization) of the thing. In this note, I would like to make a few remarks about the pervasiveness of dialectical phenomena, both in the mathematics itself as well as in the practical engagement in mathematical activity.

This post is an introduction to the container-oriented generalization of the core Brouwerian (co)data structures, inspired by Ghani, Hancock and Pattinson. I am not introducing anything novel; I’m merely taking their framework and showing how to round up the usual suspects of Brouwerian mathematics in their generalized, “family-friendly” setting. I am using Constable et al’s Computational Type Theory + Induction-Recursion as my metalanguage, but other variants of type theory may be used as well.

Here, I present a judgemental reconstruction of LCF-style tactic systems, called **Modernized LCF**, which admits various extensions including *validations* (checkable certificates). The purpose is to present the structure and meaning of refinement proof directly as a logical theory with a meaning explanation, in contrast to the standard practice of taking refinement proof as an extra-logical “finishing touch”.

This year’s Oregon Programming Languages Summer School, organized by Bob Harper, Greg Morrisett and Zena Ariola, has come to a close after two amazing weeks. I wanted to take a moment to thank everyone who made my time here so pleasant, with special regards to Bob Harper and Mark Bickford, who patiently answered my numerous questions about Nuprl and Brouwerian mathematics.

Recent conversations have convinced me that there are several misconceptions about the status of side effects in a type theoretic setting, and how to reason about their benignity. Briefly, I will clarify this matter by proposing how one might go about integrating free assignables and non-determinism into Computational Type Theory. I do not answer all questions raised by this proposal, but I intend to be provocative and suggest a rough path toward realizing this goal.

Briefly, Diaconescu’s theorem states that the axiom of choice & extensionality together suffice to imply the principle of the excluded middle (PEM). In *100 Years of Zermelo’s Axiom of Choice*, Martin-Löf distinguishes an intensional version of AC from an extensional one, and argues that whilst the former is a theorem of intuitionistic type theory, the latter leads to taboo. In this note, I hope to clarify a few matters, and demonstrate that the matter at hand is not so much extensionality, but infelicitous interpretation of quantifiers. When viewed through this lens, it becomes evident that the problem all along was setoids, not extensionality.

In 1994, Per Martin-Löf wrote Analytic and Synthetic Judgement in Type Theory, in which he convincingly showed that undecidability phenomena should be understood in terms of synthetic judgement, and demonstrated how the judgements of one theory may be made the propositions of another.

I am pleased to make available the result of joint research with Darryl McAdams, our new paper Dependent Types for Pragmatics which is currently under review for publication in the *Journal of Logic, Language and Information*. I’d like to discuss a few aspects of the work which I consider important, lending additional emphasis to foundational aspects of type theory which I fear were lost in the presentation, which was meant for a general Linguistics audience.

The key idea of Observational Type Theory is to make the *propositional* equality coextensive with the equality which is validated under the standard semantics for Type Theory, which is the meaning explanations and their metamathematical counterpart, the realizability interpretation. Now, Extensional Type Theory is usually characterized in terms of typechecking (membership) being undecidable because the “true” equality is made to hold judgementally; but this is a deceptive characterization when applied to Computational Type Theory (Nuprl), since there are many types besides equality which may be given meaning explanations but which have an undecidable membership judgement.

Whilst the judgements of type theory are preferred to be analytic, the practice of operating a proof assistant is inherently and unavoidably synthetic, and is always accompanied by some manner of refinement and tactics: and so the question is never whether to use tactics, but rather how much pain one intends to experience in the process of using them: this is inextricable from the activity of proving.

I’m so pleased to be able to announce the first fruit of a joint project with David Christiansen and Darin Morrison, which is an interview of Peter Dybjer for The Type Theory Podcast. We spoke to Peter about QuickCheck-style testing and its relation to proofs and verification in type theory. Subscribe to the RSS feed or follow us on Twitter if you are interested in listening to discussions with researchers, because we have more to come.

In my recent post I demonstrated a type-theoretic formulation of non-dependent record types as presheaves on a particular topological space \(X\) of keys given an assignment \(El_X : X\to\mathbf{Type}\). Today, I’ll construct more interesting records by endowing the key space with a non-discrete topology.

Let us define a record type as being given by a type \(X\) of **keys** and an interpretation function \(F\) which maps every key \(x:X\) to a type. We assume the existence of a powerset functor \(\mathcal{P}: \mathbf{Type}\to\mathbf{Type}\), which endows the discrete topology on \(X\). Then a record type is the product of the image of \(F\) over a subset of \(X\): \[
\mbox{for}\ U\subseteq X,\quad \mathsf{Rec}(U,F) :\equiv \prod_{s:U} F(s)
\]

To those of us without a background in topology, it may have initially been surprising that the unit circle \(S^1\) is not contractible. In this post, I’ll outline a homotopy type-theoretic proof for why this is in fact the case.

The issue of verbs which appear to take multiple arguments has long been a sticking point for Chomskyan grammarians, with various proposals having taken shape. Here, I’ll describe current approaches in transformational grammar, and demonstrate another approach in Multi-Modal Combinatorial Categorial Grammar. Finally, I’ll discuss the pros and cons of each approach.

As I read Bell’s *A Primer of Smooth Infinitesimal Analysis*, I thought it would be useful for me to write down my workings of the exercises as I went. The proofs are in the language of Intuitionistic Type Theory; according to common practice, I will sometimes omit arguments from application which can easily be inferred from the others.

Baldridge’s Multi-Modal extension of Steedman’s CCG attempts to account for variation in rule applicability entirely within the lexicon, by annotating slash types (function arrows) with modalities, which license different combining rules: \(\bullet\) licenses only simple application, \(\diamond\) simple application and harmonic composition/substitution, \(\times\) simple application and permuting composition/substitution, and \(\star\) licenses all rules. I demonstrate that further refinement is needed in order to have a grammar which suffices for the most basic hyperbata of Ancient Greek (and Latin).

Within a type-theoretic grammar, we must eventually deal with the issue of argument-ordering in languages which have (relatively) free word order. One approach, considered unsatisfactory, is to provide multiple categorial types for a word, giving the different orders in which it may accept its arguments; this is embeddable within a minimal CCG calculus. Another is to make copious use of the type raising operator combined with composition to construct mountains of unsatisfied clauses: this is less than optimal, however, given that the type raising operator itself is problematic for reasons outside the scope of this short exposition. So today, I shall present two different modest extensions to CCG which address this issue, namely *something old* and *something new*.

This is the first in a series I intend to write in regard to the syntax of Ancient Greek hyperbaton, and what can be done about it formally using a combinatory categorial grammar. We will begin with a pathological example of \(Y_1\) hyperbaton from Sophocles’ *Trachinian Women*:

τὴν Εὐρυτείαν οἶσθα δῆτα παρθένον;

the-*acc* of-Eurytus-*acc* know-*2.sing* of-course girl-*acc*

“You of course know the daughter of Eurytus…?” (*Trachinian Women*, l. 1219)

The six speeches of the *Symposium* may be divided into two sets: on the one hand, there is Phaedrus’s speech and those which are derivative of his, and on the other hand, there are the novel speeches; and these are the ones which reject the previous approaches and propose unique theories of Eros.

In this paper, I demonstrate how, and to what degree, phrase projectivity corresponds with register and meter in Sophocles’s *Antigone*, by developing a quantitative metric \(\wp\) for projectivity and comparing it across lyrics, trimeters and anapaests using the data provided by the Perseus Ancient Greek Dependency Treebank. In the appendices, the formal algorithm for the computations done herein is developed in Haskell.