Wouter Swierstra
ABSTRACT
It can be very difficult to debug impure code, let alone prove its correctness. To address these problems, we provide a functional specification of three central components of Peyton Jones's awkward squad: teletype IO, mutable state, and concurrency. By constructing an internal model of such concepts within our programming language, we can test, debug, and reason about programs that perform IO as if they were pure. In particular, we demonstrate how our specifications may be used in tandem with QuickCheck to automatically test complex pointer algorithms and concurrent programs.
- Arthur I. Baars and S. Doaitse Swierstra. Typing Dynamic Typing. In ICFP '02: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, 2002. Google Scholar
Digital Library
- Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer Verlag, 2004. Google ScholarDigital Library
- Richard Bird. Functional Pearl: Unfolding pointer algorithms. Journal of Functional Programming, 11(3):347--358, 2001. Google ScholarDigital Library
- Richard Bird and Philip Wadler. An Introduction to Functional Programming. Prentice Hall, 1988. Google ScholarDigital Library
- James Cheney and Ralf Hinze. A Lightweight Implementation of Generics and Dynamics. In Manuel Chakravarty, editor, Proceedings of the 2002 ACM SIGPLAN Haskell Workshop, pages 90--104. ACM-Press, October 2002. Google ScholarDigital Library
- Koen Claessen. A Poor Man's Concurrency Monad. In Journal of Functional Programming, volume 9, pages 313--323. Cambridge University Press, May 1999. Google Scholar
- Koen Claessen and John Hughes. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In ICFP '00: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, 2000. Google ScholarDigital Library
- Koen Claessen and John Hughes. Testing Monadic Code with QuickCheck. In Proceedings of the 2002 ACM SIGPLAN Haskell Workshop, 2002. Google ScholarDigital Library
- Nils Anders Danielsson, John Hughes, Patrik Jansson, and Jeremy Gibbons. Fast and Loose Reasoning is Morally Correct. In Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 206--217, 2006. Google ScholarDigital Library
- Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock, and Manuel M. T. Chakravarty. Running the manual: an approach to high-assurance microkernel development. In Haskell '06: Proceedings of the 2006 ACM SIGPLAN workshop on Haskell, 2006. Google ScholarDigital Library
- Neil Ghani, Peter Hancock, and Dirk Pattinson. Continuous Functions on Final Coalgebras. Electronic Notes in Theoretical Computer Science, 164(1):141--155, 2006.Google ScholarCross Ref
- Andy Gill. Debugging Haskell by Observing Intermediate Data Structures. In Proceedings of the 4th Haskell Workshop, 2000.Google Scholar
- Andrew D. Gordon. Functional Programming and Input/Output. PhD thesis, University of Cambridge, 1992.Google ScholarDigital Library
- Tim Harris, Simon Marlow, Simon Peyton Jones, and Maurice Herlihy. Composable Memory Transactions. In Proceedings of the tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 48--60, 2005. Google ScholarDigital Library
- William L. Harrison. The Essence of Multitasking. In Michael Johnson and Varmo Vene, editors, Proceedings of the 11th International Conference on Algebraic Methodology and Software Technology, volume 4019 of Lecture Notes in Computer Science, pages 158--172. Springer, 2006. Google ScholarDigital Library
- Sören Holmström. PFL: A Functional Language for Parallel Programming. In Declarative Programming Workshop, pages 114--139, 1983.Google Scholar
- Paul Hudak, Antony Courtney, Henrik Nilsson, and John Peterson. Arrows, Robots, and Functional Reactive Programming. In Summer School on Advanced Functional Programming, volume 2638 of Lecture Notes in Computer Science, pages 159--187. Springer, 2003.Google Scholar
- Graham Hutton and Joel Wright. Compiling Exceptions Correctly. In Proceedings of the 7th International Conference on Mathematics of Program Construction, volume 3125 of Lecture Notes in Computer Science. Springer, 2004.Google Scholar
- Kent Karlsson. Nebula: A Functional Operating System. Technical report, Chalmers University of Technology, 1981.Google Scholar
- David J. King and Philip Wadler. Combining monads. In John Launchbury and Patrick M. Sansom, editors, Proceedings of the Glasgow Workshop on Functional Programming, pages 134--143, Glasgow, 1992. Springer. Google ScholarDigital Library
- Sheng Liang, Paul Hudak, and Mark Jones. Monad transformers and modular interpreters. In Conference record of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 333--343, 1995. Google ScholarDigital Library
- Christoph Lüth and Neil Ghani. Composing Monads Using Coproducts. In Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming, 2002. Google ScholarDigital Library
- Conor McBride and James McKinna. The view from the left. Journal of Functional Programming, 14(1):69--111, 2004. Google ScholarDigital Library
- James McKinna and Joel Wright. A type-correct, stack-safe, provably correct, expression compiler in Epigram. Submitted to the Journal of Functional Programming, 2006.Google Scholar
- Aleksandar Nanevski and Greg Morrisett. Dependent type theory of stateful higher-order functions. Technical Report TR-24-05, Harvard University, 2005.Google Scholar
- Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. Polymorphism and separation in hoare type theory. In Proceedings of th Eleventh ACM SIGPLAN Internation Conference on Functional Programming, 2006. Google ScholarDigital Library
- Ulf Norell. Agda 2. Available online.Google Scholar
- Simon Peyton Jones. Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. In Engineering theories of software construction, 2002.Google Scholar
- Simon Peyton Jones, editor. Haskell 98 Language and Libraries - The Revised Report. Cambridge University Press, 2003.Google Scholar
- Simon Peyton Jones. Wearing the hair shirt: a retrospective on Haskell. Invited talk at the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003.Google Scholar
- Simon L. Peyton Jones and Philip Wadler. Imperative functional programming. In Conference record of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1993. Google ScholarDigital Library
- Bernard Pope. Declarative debugging with Buddha. In Summer School on Advanced Functional Programming, volume 3622 of Lecture Notes in Computer Science, pages 273--308. Springer, 2005. Google Scholar
- D. A. Turner. Total functional programming. Journal of Universal Computer Science, 10(7):751--768, 2004.Google Scholar
Index Terms
- Beauty in the beast
Recommendations
Layout-sensitive language extensibility with SugarHaskell
Haskell '12: Proceedings of the 2012 Haskell SymposiumProgrammers need convenient syntax to write elegant and concise programs. Consequently, the Haskell standard provides syntactic sugar for some scenarios (e.g., do notation for monadic code), authors of Haskell compilers provide syntactic sugar for more ...
Layout-sensitive language extensibility with SugarHaskell
Haskell '12Programmers need convenient syntax to write elegant and concise programs. Consequently, the Haskell standard provides syntactic sugar for some scenarios (e.g., do notation for monadic code), authors of Haskell compilers provide syntactic sugar for more ...
How to see the beauty that is not there: the aesthetic element of programming in the computer-based media art
OCSC'07: Proceedings of the 2nd international conference on Online communities and social computingThis study is to define aesthetic elements of the programming in the computer-based media art. It can be explained as the totality of the concept and reality in the respect of collaboration of art and science. The programming as aesthetic object ...
Comments