Pinned toot

The usual syntax for regular expressions is not a regular language because it requires parentheses. The usual syntax for context free grammars/expressions is not context-free because it uses recursion using variable names.

Is there any fundamental reason for this, i.e., some kind of diagonalization/fixed point argument or is it just a coincidence? I think the Goedelian argument doesn't apply because they are weaker than Peano arithmetic?

CBV and CBN as syntax sugar for a CBPV core language?

Everyone else has imposter syndrome but I am the one person who actually is just lucky/a fraud.

Hard-core Curry-style/extrinsic typing advocate gives checks for unbalanced parentheses at runtime

Doing advent of code with a toy/young language:

Expectation: Time to implement some cool data structures!
Reality: Time to write lexers/parsers! (Either by hand or implement some parsing libraries)

According to Eilenberg and Mac Lane, they created category theory in 1945 to be able to define natural transformation, a notion that existed in the air at that time but had no definition.

But I think that the real purpose of category theory is to define the notion of universal property. Which also had traces at that time (e.g. in the desired properties of function spaces, already in 1935 in a letter of Hurewicz to Fox).

This is from the classic "Lambda: The Ultimate GOTO" paper. Sad that this is only taken seriously in functional languages to this day and we have new platforms like WASM that don't take advantage of this lesson.

Also, this is exactly how CBPV works.
1. `GOTO` is in CPBV `force`ing a thunk,
2. Pushing a return address onto the stack corresponds to the "bind" `x <- M; N` construct. You push the kont `x. N` onto the stack.

Advent of Code Day 1 

We have hardly anything implemented so it ended up looking like assembly code but here's day 1 solution in our CBPV language Zydeco:

Probably won't be able to keep this up very long since we haven't implemented parameterized datatypes, polymorphism or even imports yet but it was fun to get the very easy one working.

Compilers Class Musings 

Close to finishing my first compilers course where I actually teach parsing/front-end in some depth. While I think there is usually over emphasis of particular algorithms over general principles, I was struck by the fact that the front-end is treated much more systematically and mathematically than the backend: different front end passes (lexing/parsing/type checking) are given mathematical specifications in terms of grammars/declarative type systems and then we need an algorithm to implement the spec.

Compare the backend where specs are usually very informal and so correctness is fuzzier. It's a bit funny bc most of my research is on semantics that only applies to the backend. But perhaps that's exactly why we emphasize mathematical specification of the front-end more: because it's already been figured out while the backend is research or at least involves more PL semantics than we can fit without a prereq.

Anyway at least this gave me the idea to give my last lecture on compiler correctness and verification and to frame it in these terms.

@burakemir @shriramk @joomy

This is not a shitpost thank you.

A regexp is a logical formula with denotation in a set of "non standard truth values": the poset of predicates on strings rather than classical truth values {top, bot}. Empty and alternatives denote the bottom element and the join of this poset. Regular languages are closed under intersection so it is ok to add in conjunction as well. Kleene star is a particular LFP. The characters are atomic formulae and the empty string/sequencing are interpreted as a nice monoidal structure of the poset of languages (Day convolution).

A different way to say this is that regular expressions can all be interpreted as formulae in a non-symmetric variant of the logic of bunched implications where the sequencing is the *.

Regular Expressions : Logic Programming :: DFA : Functional Programming ?

Very bizarre that Rust's test lib supports Result<T, String> as an output type but then doesn't display that string in the error message if the test fails. Should probably just use some unit testing crate that provides a better interface.

What prospective advisors are looking for Ph.D. applicants who want to work on compilers? I know about the usual suspects, but would love to have more names to offer the undergrad I'm advising, especially new/junior faculty working on building a lab.

Ugh after the utter schlock that has been coming out of Disney Star Wars for years now finally they make a good show (Andor)? I'm so skeptical but everyone is saying it's so great...

In the spirit of "teaching category theory in the context of applications" my category theory course for next semester is somewhat morphing into an axiomatic + denotational semantics course.

I haven’t done an #introduction yet, which seems to be a thing here, so:

Hi I’m Chris! I’m a prof at Northeastern (newly tenured!) researching computational tools for #gamedev, #generativeart, #storytelling, and collaborative co-creativity using PL/logic and HCI methods.

I’m neurodivergent, nonbinary, and my politics are heavily informed by Indigenous, Black, Trans and Disabled thinkers towards decolonization and anarchist interdependency.


Maths and PL friends. We have PhD-student scholarships available at the University of Birmingham, UK.

In particular, Eric Finster, Vincent Rahli and myself would be very interested in getting students in type theory, homotopy theory, higher-categories, constructive mathematics, and related fields.

Please encourage your best students to apply.

Or, if you are a student reading this, consider applying:

The main lesson from PER semantics of PLs is that the purpose of types is to exclude and confuse.

There's a special place in hell for people who design a new target for language implementation that doesn't support tail calls/goto...get ur act together WASM

Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.