xmonad in Coq (experience report): programming a window manager in a proof assistant
Abstract
References
Index Terms
- xmonad in Coq (experience report): programming a window manager in a proof assistant
Recommendations
xmonad in Coq (experience report): programming a window manager in a proof assistant
Haskell '12: Proceedings of the 2012 Haskell SymposiumThis report documents the insights gained from implementing the core functionality of xmonad, a popular window manager written in Haskell, in the Coq proof assistant. Rather than focus on verification, this report outlines the technical challenges ...
Parametric higher-order abstract syntax for mechanized semantics
ICFP '08We present parametric higher-order abstract syntax (PHOAS), a new approach to formalizing the syntax of programming languages in computer proof assistants based on type theory. Like higher-order abstract syntax (HOAS), PHOAS uses the meta language's ...
Parametric higher-order abstract syntax for mechanized semantics
ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programmingWe present parametric higher-order abstract syntax (PHOAS), a new approach to formalizing the syntax of programming languages in computer proof assistants based on type theory. Like higher-order abstract syntax (HOAS), PHOAS uses the meta language's ...
Comments
Information & Contributors
Information
Published In
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations2Total Citations
- 264Total Downloads
- Downloads (Last 12 months)2
- Downloads (Last 6 weeks)0
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in