If You Build It, They Will Come
Technical Reports by Steven Obua
July 29th, 2021
These are preliminary notes about Practal’s logic and its system of practical types. This is ongoing research, and I expect updates to this document over time. Practal Light is a research prototype implementing (part of) what is presented in this document.
July 17th, 2021
Practal — Practical Logic
This is a ﬁrst sketch of the design of Practal, an interactive theorem proving system for practical logic.
July 1st, 2021
I propose a simple Unicode-based lexical syntax for programming language identiﬁers using characters from international scripts (currently Latin, Greek, Cyrillic and Math). Such cosmopolitan identiﬁers are designed to achieve much of the simplicity of Fortran identiﬁers while acknowledging a modern international outlook. This seems particularly advantageous in contexts where such identiﬁers are not (only) used by professional programmers, but are exposed to normal users, for example through scriptable applications.
May 18th, 2021
A New Semantics for Local Lexing
A revised semantics for Local Lexing is presented that entirely avoids priority conﬂicts between non-empty tokens. Pyramid Grammars are introduced, and their semantics is given in terms of Local Lexing. It is demonstrated that they are more expressive than Context-Free Grammars, and at least as expressive as Parsing Expression Grammars.