We introduce Generalised Object Normal Form (GONF), a syntax formalism that enables language designers to define concrete syntax in a form that also naturally defines the data structure of the abstract syntax tree. More precisely, GONF's grammatical productions specify simultaneously and without annotations (1) concrete syntax (a language and its parser) and (2) the collection of language-independent data type definitions representing the abstract syntax tree accurately and concisely. These types can be materialised in languages supporting inheritance or algebraic types, and preferably parametric polymorphism. We also describe MTP, an available GONF-based tool.
This paper reports an investigation into the link between failed proofs and non-theorems. It seeks to answer the question of whether anything more can be learned from a failed proof attempt than can be discovered from a counter-example. We suggest that the branch of the proof in which failure occurs can be mapped back to the segments of code that are the culprit, helping to locate the error. This process of tracing provides finer grained isolation of the offending code fragments than is possible from the inspection of counter-examples. We also discuss ideas for how such a process could be automate
We explain the gist of how to attain side effects in pure functional programming languages via monads and unique types with input-output as a motivating example. Our vehicle for illustration is the strongly type-checked, pure, and non-strict functional language Haskell. The category-theoretical origins of monads are explained. Some basic notions of Category Theory are also presented in programming terms. We provide a list of suggested reading material in the references
This file was generated by bibtex2html 1.98.