I was reading a paper (PDF) that introduced a term, internal syntax, that I've never heard of. What does this term mean, and how is it different from the source syntax?
It looks that the internal syntax is used to formally prove some properties about the language (at least in this paper). I'd like to know the exact definition and the background behind this syntax.
In your linked example paper, what the auther refers to as Internal Syntax is merely the grammar of the language, in this case expressed in the common EBNF (Extended Backus-Naur Form) notation.
It is a formal representation of the allowable constructs and how they can appear in the source file of the language, as it defines how the various keywords and other language items can and cannot appear in order to have a valid file.
Entering in BNF and the name of your favorite language should likely return many hits on any search engine, and may allow an easier entry to the concept of language grammar with some familiarity due to your recognizing the various keywords and the like.
Enjoy!
They're calling it "internal syntax" to contrast it with the syntax of previous examples, which are written in a semicolons-and-braces syntax.
See the first paragraph of section 4:
We start by describing the syntax and object model of a core language, which is intended to be simpler than Plaid source code yet be capable of representing all of the major semantic elements of Plaid.
It is typical in programming languages research to talk about a real language in terms of a core language model. The real language is often verbose, and it has many features necessary for getting work done that have nothing to do with the specific point of the paper. Given that most languages are developed as extensions of existing languages, it may have inherited its syntactic and/or semantic complexity from the language it's based on. The core language, in contrast, is designed to be really terse and simple, to have only enough features to illustrate the paper's point. For example, in MacQueen's paper on the ML module system, he models ML with a dependently-typed lambda calculus called SOL. ML has I/O, exceptions, and all sorts of other features; SOL doesn't, because they aren't necessary to explain how the module system works.
