String Literals

The first level is the string literal calculus D^String_Lit. For example, text files (left) and string literals (right) are both examples of document languages at this level:

left:

I'm suspicious of "strings".

right:

"I'm suspicious of \"strings\"."

Formally, D^String_Lit has no Computation and therefore the simplest semantics:

Expr^String_Lit 𝜀 ::= s Type^String_Lit 𝜏 ::= String

A string s ∈ String is a sequence of characters c ∈ Char, such as “x” or […]. We will present a sequence of document calculi D^String_. in the string domain.

~

CRICHTON, Will and KRISHNAMURTHI, Shriram, 2024. A Core Calculus for Documents: Or, Lambda: The Ultimate Document. Proceedings of the ACM on Programming Languages. 5 January 2024. Vol. 8, no. POPL, p. 23:667-23:694. doi , p. 23:6.