LNgen: Tool Support for Locally Nameless Representations (2009)
Brian Aydemir, Stephanie Weirich
Given the complexity of the metatheoretic reasoning involved with current programming languages and their type systems, techniques for mechanical formalization and checking of the metatheory have...
Aydemir, Brian, Zdancewic, Stephan A, Weirich, Stephanie
Binding is a fundamental part of language specification, yet it is both difficult and tedious to get right. In previous work, we argued that an approach based on locally nameless representation and a...
Process Migration and Transactions Using a Formal Intermediate Language ∗ ABSTRACT (2008)
Jason Hickey, Justin D. Smith, Brian Aydemir, Nathaniel Gray, Adam Granicz, Cristian T Ăpus
Process migration and atomic transactions are essential tools for constructing fault-tolerant distributed systems. Process migration provides location transparency, the ability to perform...
Formal Design Environments (2008)
Brian Aydemir, Adam Granicz, Jason Hickey
Abstract. We present the design of a formal integrated design environment. The long-term goal of this effort is to allow seamless interaction between software production tools and formal design and...
Nominal Reasoning Techniques in Coq (Extended Abstract) (2008)
Brian Aydemir, Aaron Bohannon, Stephanie Weirich
We explore an axiomatized nominal approach to variable binding in Coq, using an untyped lambda-calculus as our test case. In our nominal approach, alpha-equality of lambda terms coincides with...
Engineering Formal Metatheory (2008)
Aydemir, Brian, Charguéraud, Arthur, Pierce, Benjamin C, Pollack, Randy, Weirich, Stephanie
Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and as a foundation for technologies such as...
Engineering formal metatheory (2008)
Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and as a foundation for technologies such as...
Engineering formal metatheory (2008)
Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and as a foundation for technologies such as...
Engineering formal metatheory (2008)
Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Y Pollack, Stephanie Weirich
Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and as a foundation for technologies such as...
Engineering formal metatheory (2008)
Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and as a foundation for technologies such as...
A Listing of MetaPRL Theories 1 (2007)
Jason Hickey, Brian Aydemir, Yegor Bryukhov, Alexei Kopylov, Aleksey Nogin, Xin Yu
This document contains a listing of most of the MetaPRL logical theories. It is generated automatically on a daily basis. To get the latest version, go to
Formal Design Environments (2007)
Brian Aydemir, Adam Granicz, Jason Hickey
Abstract. We present the design of a formal integrated design environment. The long-term goal of this eort is to allow seamless interaction between software production tools and formal design and...
A Listing of MetaPRL Theories 1 (2006)
Jason Hickey, Brian Aydemir, Yegor Bryukhov, Alexei Kopylov, Aleksey Nogin, Xin Yu
This document contains a listing of most of the MetaPRL logical theories. It is generated automatically on a daily basis. To get the latest version, go to
Formal Compiler Implementation in a Logical Framework (2003)
Hickey, Jason, Nogin, Aleksey, Granicz, Adam, Aydemir, Brian
The task of designing and implementing a compiler can be a dicult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term rewriting...
Formal compiler implementation in a logical framework (2003)
Jason Hickey, Aleksey Nogin, Adam Granicz, Brian Aydemir
The task of designing and implementing a compiler can be a dicult and error-prone process. In this paper, we present syntax and term rewriting in a logical framework. All program transformations,...
Formal compiler implementation in a logical framework (2003)
Jason Hickey, Aleksey Nogin, Adam Granicz, Brian Aydemir
The task of designing and implementing a compiler can be a dicult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term rewriting...
Formal Compiler Implementation in a Logical Framework (2003)
Jason Hickey, Aleksey Nogin, Adam Granicz, Brian Aydemir
The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term...
Compiler Implementation in a Formal Logical Framework (2003)
Jason Hickey, Aleksey Nogin, Adam Granicz, Brian Aydemir
The task of designing and implementing a compiler can be a dicult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term rewriting...
Compiler implementation in a formal logical framework (2003)
Jason Hickey, Aleksey Nogin, Adam Granicz, Brian Aydemir
The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present syntax and term rewriting in a logical framework. All program transformations,...
Process Migration and Transactions Using a Novel Intermediate Language (2002)
Hickey, Jason, Smith, Justin D., Aydemir, Brian, Gray, Nathaniel, Granicz, Adam, Tapus, Cristian
Process migration and transactions using a novel intermediate language (2002)
Jason Hickey, Justin D. Smith, Brian Aydemir, Nathaniel Gray, Adam Granicz, Cristian Tapus
Process migration and atomic transactions are essential tools for constructing fault-tolerant distributed systems. We present a new system that includes a typed intermediate language and runtime...
Formal Compiler Implementation in a Logical Framework (1998)
Hickey, Jason, Nogin, Aleksey, Granicz, Adam, Aydemir, Brian
The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present a new approach based on the use of higher-order abstract syntax and term...