skip to main content
10.1145/2364506.2364523acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
research-article

xmonad in Coq (experience report): programming a window manager in a proof assistant

Published: 13 September 2012 Publication History

Abstract

This 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 involved with incorporating Coq code in a Haskell project.

References

[1]
E. Brady. Practical Implementation of a Dependently Typed Functional Programming Language. PhD thesis, Durham University, 2005.
[2]
E. Brady. Idris - systems programming meets full dependent types. In PLPV'11: Proceedings of the 2011 ACM SIGPLAN Workshop on Programming Languages meets Programming Verification, 2011.
[3]
A. Chlipala. Certified programming with dependent types. Available from http://adam.chlipala.net/cpdt, 2008.
[4]
K. Claessen and J. Hughes. QuickCheck: a lightweight tool for random testing of Haskell programs. In Proceedings of the fifth ACM SIGPLAN International Conference on Functional Programming, 2000.
[5]
T. Coquand and G. Huet. The calculus of constructions. Inf. Comput., 76: 95--120, February 1988.
[6]
L. Cruz-Filipe, H. Geuvers, and F. Wiedijk. C-CoRN, the constructive Coq repository at Nijmegen. In Mathematical Knowledge Management, 2004.
[7]
E. Denney. The synthesis of a Java Card tokenization algorithm. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering, 2001.
[8]
P. Derrin, K. Elphinstone, G. Klein, D. Cock, and M. M. T. Chakravarty. Running the manual: An approach to high-assurance microkernel development. In Proceedings of the ACM SIGPLAN Haskell Workshop, 2006.
[9]
J.-C. Filliâtre and P. Letouzey. Functors for Proofs and Programs. In Proceedings of The European Symposium on Programming, volume 2986 of Lecture Notes in Computer Science, 2004.
[10]
A. Gill and C. Runciman. Haskell Program Coverage. In Proceedings of the ACM SIGPLAN Workshop on Haskell, 2007.
[11]
G. Gonthier. Formal proof: the four-color theorem. Notices of the AMS, 55 (11): 1382--1393, 2008.
[12]
B. Grégoire. Compilation des termes de preuves: un (nouveau) mariage entre Coq et OCaml. PhD thesis, Université Paris 7, 2003.
[13]
F. Haftmann. From higher-order logic to Haskell: there and back again. In Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pages 155--158, 2010.
[14]
G. Huet. The zipper. Journal of Functional Programming, 7 (05): 549--554, 1997.
[15]
G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, et al. seL4: Formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pages 207--220. ACM, 2009.
[16]
X. Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 42--54, 2006.
[17]
P. Letouzey. A new extraction for Coq. Types for Proofs and Programs, 2003.
[18]
P. Letouzey. Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq. PhD thesis, Université Paris-Sud, 2004.
[19]
P. Letouzey. Personal communication. 2011.
[20]
P. Martin-Löf. Constructive mathematics and computer programming. Studies in Logic and the Foundations of Mathematics, 104, 1982.
[21]
The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004. URL http://coq.inria.fr.
[22]
C. McBride. Dependently typed functional programs and their proofs. PhD thesis, University of Edinburgh, 1999.
[23]
N. Mitchell. HLint Manual, 2010.
[24]
N. Mitchell and C. Runciman. Not all patterns, but enough: an automatic verifier for partial but sufficient pattern matching. In Proceedings of the first ACM SIGPLAN Symposium on Haskell, 2008.
[25]
U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007.
[26]
M. Sozeau. Programing Finger Trees in Coq. In ICFP'07: Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming, pages 13--24, 2007a.
[27]
M. Sozeau. Subset coercions in Coq. In T. Altenkirch and C. McBride, editors, Types for Proofs and Programs, volume 4502 of Lecture Notes in Computer Science, pages 237--252. Springer, 2007b.
[28]
M. Sozeau and N. Oury. First-class type classes. In Theorem Proving in Higher Order Logics, 2008.
[29]
D. Stewart. Popular haskell packages: Q2 2010 report, June 2010. URL http://donsbot.wordpress.com/.
[30]
D. Stewart and S. Janssen. xmonad: a tiling window manager. In Proceedings of the ACM SIGPLAN Workshop on Haskell, 2007.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
Haskell '12: Proceedings of the 2012 Haskell Symposium
September 2012
168 pages
ISBN:9781450315746
DOI:10.1145/2364506
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 47, Issue 12
    Haskell '12
    December 2012
    157 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2430532
    Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 September 2012

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. coq
  2. dependent types
  3. formal verification
  4. functional programming
  5. haskell
  6. interactive proof assistants
  7. program extraction
  8. xmonad

Qualifiers

  • Research-article

Conference

ICFP'12
Sponsor:

Acceptance Rates

Overall Acceptance Rate 57 of 143 submissions, 40%

Upcoming Conference

ICFP '25
ACM SIGPLAN International Conference on Functional Programming
October 12 - 18, 2025
Singapore , Singapore

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)2
  • Downloads (Last 6 weeks)0
Reflects downloads up to 27 Jan 2025

Other Metrics

Citations

Cited By

View all

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media