Category Archives: Geometry of Synthesis

Categorical semantics of digital circuits

Isn’t it funny that the world of programming languages is defined by syntax while the world of circuit design is defined by semantics? One can never be sure, but it seems to me that when people design software they imagine the … Continue reading

Posted in Geometry of Synthesis | 1 Comment

Two consequences of full abstraction

In a recent paper [pdf] with my student Zaid Al-Zobaidi we describe two enhancements to the GoI compiler. The first one is a tamper-proof mechanism which guarantees that no low-level attacks against the compiled code are possible. This is very nice … Continue reading

Posted in game semantics, Geometry of Synthesis, system level semantics | 1 Comment

Remember machine-independence?

An interesting quotation from Dijkstra, written in 1961: I would require of a programming language that it should facilitate the work of the programmer as much as possible, especially in the most difficult aspects of his task, such as creating … Continue reading

Posted in Geometry of Synthesis | Leave a comment

Verity now with call-by-value

Call-by-name is generally seen as an annoyance by programmers. Fortunately, if your programming language has mutable state you can force evaluation at ground type by using assignment, so by writing new v in v := x; f(!v) you achieve the … Continue reading

Posted in Geometry of Synthesis | Leave a comment

Back to the future

The programming language ALGOL was “a language so far ahead of its time, that it was not only an improvement on its predecessors, but also on nearly all its successors,” at least according to C.A.R. Hoare. Few programming languages have been … Continue reading

Posted in Geometry of Synthesis | 2 Comments

Talk at “Compiling Complete Programs into Circuits” 2012

I gave a contributed talk on GOS/Verity at the CCPC workshop, part of the ASPLOS conference. The focus of the talk was on the fact that using a semantic notion of function call it is possible to support separate compilation … Continue reading

Posted in Geometry of Synthesis | Leave a comment

Global state considered a fiction

Here is what my colleague Uday Reddy says in his paper “Global State Considered Unnecessary” [pdf]: The traditional semantics of imperative features is based on the notion of global store. A variable is an index into the store and the store … Continue reading

Posted in game semantics, Geometry of Synthesis | Leave a comment

Separate compilation in higher-level synthesis

The Geometry of Synthesis [pdf] research programme aims to develop higher-level synthesis tools and techniques that bring full support for functions. On the language side this means things like higher-order functions [pdf] and recursion [pdf]. On the compiler side this … Continue reading

Posted in Geometry of Synthesis | Leave a comment