Drafts
-
LNgen: Tool Support for Locally Nameless
Representations. Brian Aydemir and Stephanie Weirich. October
2009.
[ pdf
| home page
]
(Coq formalizations are included with the LNgen distribution.)
Conference and workshop papers
-
Engineering Formal Metatheory.
Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy
Pollack, and Stephanie Weirich. In POPL '08: Proceedings of the
35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, 3–15. ACM, 2008.
[ pdf
| Coq code
]
-
Nominal Reasoning Techniques in Coq
(Extended Abstract). Brian Aydemir, Aaron Bohannon, and
Stephanie Weirich. In Proceedings of the First International
Workshop on Logical Frameworks and Meta-Languages: Theory and
Practice (LFMTP 2006), edited by Alberto Momigliano and Brigitte
Pientka, volume 174 of Electronic Notes in Theoretical Computer
Science, 69–77. Elsevier, 2007.
[ pdf
| slides
| Coq 8.2 code (.tar.gz)
| Coq code (HTML)
]
-
Mechanized Metatheory for the Masses:
The PoplMark
Challenge. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn,
J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios
Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve
Zdancewic. In Theorem Proving in Higher Order Logics: 18th
International Conference, TPHOLs 2005, volume 3603 of Lecture
Notes in Computer Science, edited by Joe Hurd and Tom Melham,
50–65. Springer, 2005.
[ pdf
| pdf with appendices
| home page
]
-
MetaPRL — A Modular Logical Environment. Jason Hickey,
Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay,
Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov,
Christoph Kreitz, Vladimir N. Krupski, Lori Lorigo, Stephan Schmitt,
Carl Witty, and Xin Yu. In Theorem Proving in Higher Order
Logics: 16th International Conference, TPHOLs 2003, edited by
David Basin and Burkhart Wolff, volume 2758 of Lecture Notes in
Computer Science, 287–303. Springer, 2003.
[ pdf
| home page
]
-
Formal Design Environments. Brian Aydemir, Adam Granicz, and
Jason Hickey. In Track B Proceedings of the 15th International
Conference on Theorem Proving in Higher Order Logics (TPHOLs
2002), edited by Victor A. Carreño, Cézar
A. Muñoz, and Sophiène Tahar, 12–22. NASA, 2002.
[ pdf
]
Technical reports