Prototyping a query compiler using Coq
Joshua S. Auerbach, Martin Hirzel, et al.
JFLA 2017
In the Concert multilanguage distributed programming system, interface specification is the responsibility of programming languages, not a separate IDL. However, an IDL is still necessary in order to define equivalence between declarations in different languages. A single representation is also desirable internally to economize on aspects of the implementation. Consequently, Concert has an IDL as an intermediate language, produced by compiler front-ends and not normally manipulated by programmers. It is formally separated into a contract, which defines interoperability and an endpoint modifier, which captures the local choice of representation. Only contracts are used to define interface equivalence. Our choice of what kinds of information to put in the contract was motivated by a desire to be minimal, thereby enabling maximum feasible interoperability between different expressions of the same abstraction in the same or different languages. © 1994, ACM. All rights reserved.
Joshua S. Auerbach, Martin Hirzel, et al.
JFLA 2017
Joshua S. Auerbach, Martin Hirzel, et al.
SIGMOD 2017
Erik Altman, Joshua S. Auerbach, et al.
FPT 2013
Joshua S. Auerbach, Martin Hirzel, et al.
SIGMOD 2017