Personal tools

Research papers/Testing and correctness

From HaskellWiki

< Research papers(Difference between revisions)
Jump to: navigation, search
(link across to verfified kernels)
m (Adding new paper to the security section)
 
(15 intermediate revisions by 7 users not shown)
Line 1: Line 1:
 
 
__TOC__
 
__TOC__
   
Line 40: Line 39:
 
:Koen Claessen, Colin Runciman, Olaf Chitil, and John Hughes. In Advanced Functional Programming: 4th International School, Lecture Notes in Computer Science, vol. 2638, pp. 59--99, Springer Verlag, 2002.
 
:Koen Claessen, Colin Runciman, Olaf Chitil, and John Hughes. In Advanced Functional Programming: 4th International School, Lecture Notes in Computer Science, vol. 2638, pp. 59--99, Springer Verlag, 2002.
   
;[http://www.cambridge.intel-research.net/~rennals/talk_hsdebug.pdf HsDebug: Debugging Lazy Programs by Not Being Lazy]
+
;[http://berkeley.intel-research.net/rennals/pubs/hw2003.pdf HsDebug: Debugging Lazy Programs by Not Being Lazy]
 
:Robert Ennals and Simon Peyton-Jones. Cambridge University, Microsoft Research.
 
:Robert Ennals and Simon Peyton-Jones. Cambridge University, Microsoft Research.
   
;[http://www.cs.mu.oz.au/~bjpop/thesis.ps.gz Buddha: A Declarative Debugger for Haskell]
+
;[http://www.cs.mu.oz.au/~bjpop/buddha/ Buddha: A Declarative Debugger for Haskell]
:By Bernie Pope. Honours Thesis.
+
:By Bernie Pope.
   
 
;[http://www.cs.bris.ac.uk/Publications/Papers/1000398.pdf Augmenting Trace-based Functional Debugging]
 
;[http://www.cs.bris.ac.uk/Publications/Papers/1000398.pdf Augmenting Trace-based Functional Debugging]
 
:Alastair Penney. PhD. Thesis. University of Bristol. September 1999.
 
:Alastair Penney. PhD. Thesis. University of Bristol. September 1999.
  +
  +
;[http://www.cs.kent.ac.uk/pubs/2006/2367/index.html Towards a theory of tracing for functional programs based on graph rewriting]
  +
:Olaf Chitil and Yong Luo. In Ian Mackie, editor, Draft Proceedings of the 3rd International Workshop on Term Graph Rewriting, Termgraph 2006, page 10, April 2006.
  +
  +
;[http://www.cs.kent.ac.uk/pubs/2001/1810/index.html A semantics for tracing. Olaf Chitil]
  +
:In Thomas Arts and Markus Mohnen, editors, Draft Proceedings of the 13th International Workshop on Implementation of Functional Languages, IFL 2001, pages 249-254, lvsj, Sweden, September 2001. Ericsson Computer Science Laboratory.
   
 
==Testing==
 
==Testing==
Line 68: Line 73:
 
;[http://www.cs.unc.edu/~heringto/HUnit/ Unit Testing with HUnit]
 
;[http://www.cs.unc.edu/~heringto/HUnit/ Unit Testing with HUnit]
 
:Dean Herington. 2002.
 
:Dean Herington. 2002.
  +
  +
;[http://www.cs.kent.ac.uk/pubs/2003/1808/index.html Lazy assertions]
  +
:Olaf Chitil, Dan McNeill, and Colin Runciman. In Draft Proceedings of the 15th International Workshop on Implementation of Functional Languages, IFL 2003, pages 31-46, Edinburgh, Scotland, September 2003.]
  +
  +
;[http://www.ituniv.se/program/sem_research/Publications/2006/AHJW06/ Testing Telecoms Software with Quviq QuickCheck]
  +
:Thomas Arts, John Hughes, Joakim Johansson, Ulf Wiger, Proceedings of the Fifth ACM SIGPLAN Erlang Workshop - 2006
   
 
==Verifying Haskell programs==
 
==Verifying Haskell programs==
   
;[http://www.cs.ukc.ac.uk/pubs/1992/123/index.html Formulating Haskell]
+
;[http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm Static contract checking for Haskell]
:[http://www.cs.ukc.ac.uk/people/staff/sjt/index.html Simon Thompson]. Technical Report 29-92*, University of Kent, Computing Laboratory, University of Kent, Canterbury, UK, November 1992.
+
:Dana Xu and Simon Peyton Jones, POPL 2009.
  +
  +
;[http://www.cs.kent.ac.uk/pubs/1992/123/index.html Formulating Haskell]
  +
:[http://www.cs.kent.ac.uk/people/staff/sjt/index.html Simon Thompson]. Technical Report 29-92*, University of Kent, Computing Laboratory, University of Kent, Canterbury, UK, November 1992.
   
 
;[http://www.cs.chalmers.se/~makoto/qsic03.pdf Verifying Haskell Programs by Combining Testing and Proving]
 
;[http://www.cs.chalmers.se/~makoto/qsic03.pdf Verifying Haskell Programs by Combining Testing and Proving]
Line 80: Line 91:
 
:Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell. Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, Tallinn, Estonia 62-73, 2005, ISBN 1-59593-071-X
 
:Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell. Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, Tallinn, Estonia 62-73, 2005, ISBN 1-59593-071-X
   
;[http://www.cs.pdx.edu/~sheard/papers/PutCurryHoward2WorkFinalVersion.ps Putting Curry-Howard to Work]
+
;[http://web.cecs.pdx.edu/~sheard/papers/PutCurryHoward2WorkFinalVersion.ps Putting Curry-Howard to Work]
 
:Tim Sheard, Proceedings of the 2005 ACM SIGPLAN workshop on Haskell. Tallinn, Estonia, 74 - 85, 2005 ISBN 1-59593-071-X
 
:Tim Sheard, Proceedings of the 2005 ACM SIGPLAN workshop on Haskell. Tallinn, Estonia, 74 - 85, 2005 ISBN 1-59593-071-X
   
 
;[http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps Extended Static Checking for Haskell]
 
;[http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps Extended Static Checking for Haskell]
 
:Dana Xu, Haskell Workshop 2006
 
:Dana Xu, Haskell Workshop 2006
  +
  +
;[http://www-users.cs.york.ac.uk/~ndm/downloads/paper-unfailing_haskell_a_static_checker_for_pattern_matching-24_sep_2005.pdf Unfailing Haskell: A static checker for pattern matching]
  +
:Neil Mitchell, Colin Runciman, Trends in Functional Programming 2005.
  +
  +
;[http://web.comlab.ox.ac.uk/people/Jeremy.Gibbons/publications/acmmpc-optimization.pdf Algebraic methods for optimization problems]
  +
:Richard Bird, Jeremy Gibbons, and Shin Cheng Mu. In Roland Backhouse, Roy Crole, and Jeremy Gibbons, editors, Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, volume 2297 of Lecture Notes in Computer Science, pages 281-307. Springer-Verlag, 2002.
  +
  +
;[http://ropas.snu.ac.kr/~kwang/paper/06-jfp-yi.pdf Proof-directed debugging: revisited]
  +
:Kwangkeun Yi. JFP. 16(6):663-670
  +
  +
;[http://web.archive.org/web/20080120074832/http://www.comp.nus.edu.sg/~sulzmann/publications/plpv06-langverification.ps Language-Based Program Verification via Expressive Types]
  +
:Martin Sulzmann and Razvan Voicu. In Programming Languages meet Program Verification (PLPV'06)
  +
  +
;[http://wwwtcs.inf.tu-dresden.de/~voigt/pepm09-voigtlaender.pdf Proving Correctness via Free Theorems: The Case of the destroy/build-Rule]
  +
:Janis Voigtländer. Workshop on Partial Evaluation and Program Manipulation (PEPM'08), Proceedings, ACM Press, 2008.
  +
  +
  +
===Security===
  +
; [http://www.cse.chalmers.se/~russo/publications_files/haskell11.pdf Flexible Dynamic Information Flow Control in Haskell]
  +
:Deian Stefan, Alejandro Russo, John Mitchell, and David Mazieres.
  +
  +
; [http://www.cse.chalmers.se/~russo/ Secure Multi-Execution in Haskell]
  +
:Mauro Jaskelioff, Alejandro Russo.
  +
  +
; [http://www.cse.chalmers.se/~russo/ A Library for Light-weight Information-Flow Security in Haskell]
  +
:Alejandro Russo, Koen Claessen, John Hughes.
  +
  +
; [http://www.cse.chalmers.se/~russo/ A Library for Secure Multi-threaded Information Flow in Haskell]
  +
:Ta-chung Tsai, Alejandro Russo, John Hughes.
  +
  +
; [http://www.cis.upenn.edu/~stevez/papers/LZ06a.pdf Encoding Information Flow in Haskell]
  +
  +
; [http://www.seas.upenn.edu/~lipeng/homepage/papers/lz06tcs.pdf Arrows for Secure Information Flow]
   
 
See also work on [[Research_papers/Program_development#Operating_systems|verifying microkernels in Haskell]]
 
See also work on [[Research_papers/Program_development#Operating_systems|verifying microkernels in Haskell]]
Line 92: Line 136:
 
;[http://www.informatik.uni-bonn.de/~ralf/publications/Contract.pdf Typed Contracts for Functional Programming]
 
;[http://www.informatik.uni-bonn.de/~ralf/publications/Contract.pdf Typed Contracts for Functional Programming]
 
:Ralf Hinze, Johan Jeuring and Andres Lh. In Philip Wadler and Masimi Hagiya, editors, Proceedings of the Eighth International Symposium on Functional and Logic Programming (FLOPS 2006), 24-26 April 2006, Fuji Susono, Japan.
 
:Ralf Hinze, Johan Jeuring and Andres Lh. In Philip Wadler and Masimi Hagiya, editors, Proceedings of the Eighth International Symposium on Functional and Logic Programming (FLOPS 2006), 24-26 April 2006, Fuji Susono, Japan.
  +
  +
[[Category:Research]]

Latest revision as of 21:18, 13 July 2011

Contents


[edit] 1 Tracing and debugging

Freja, Hat and Hood - A Comparative Evaluation of Three Systems for Tracing and Debugging Lazy Functional Programs
Olaf Chitil, Colin Runciman, and Malcolm Wallace. Proceedings of the 12th International Workshop on Implementation of Functional Languages, Aachen, Germany, September 4th - 7th 2000, LNCS 2011, 2001, pp. 176--193
Multiple-View Tracing for Haskell - a New Hat
Malcolm Wallace, Olaf Chitil, Thorsten Brehm, and Colin Runciman. (draft)
Lazy algorithmic debugging: ideas for practical implementation.
Henrik Nilsson and Peter Fritzson. In Peter Fritzson, editor, Automated and Algorithmic Debugging, volume 749 of Lecture Notes in Computer Science, pages 117 - 134, Linkping, Sweden, May 1993.
Henrik Nilsson and Peter Fritzson.
Algorithmic debugging for lazy functional languages. Journal of Functional Programming, 4(3):337 - 370, July 1994.
A declarative approach to debugging for lazy functional languages.
Henrik Nilsson. Licentiate Thesis No. 450, Department of Computer and Information Science, Linkpings universitet, S-581 83, Linkping, Sweden, September 1994.
The architecture of a debugger for lazy functional languages.
Jan Sparud and Henrik Nilsson. In Mireille Ducass, editor, Proceedings of AADEBUG '95, 2nd Internatinal Workshop on Automated and Algorithmic Debugging, Saint-Malo, France, May 1995, IRISA, Campus Universitaire de Beaulieu, 35042 Rennes, Cedex, France.
The evaluation dependence tree: an execution record for lazy functional debugging
Henrik Nilsson and Jan Sparud. Research Report LiTH-IDA-R-96-23, Department of Computer and Information Science, Linkpings universitet, S-581 83, Linkping, Sweden, August 1996.
The evaluation dependence tree as a basis for lazy functional debugging
Henrik Nilsson and Jan Sparud. Automated Software Engineering, 4(2):121 - 150, April 1997.
Declarative Debugging for Lazy Functional Languages
Henrik Nilsson. PhD Thesis No. 430, Department of Computer and Information Science, Linkpings universitet, S-581 83, Linkping, Sweden, May 1998.
Tracing piece by piece: affordable debugging for lazy functional languages
Henrik Nilsson. Proceedings of the 1999 ACM SIGPLAN International Conference on Functional Programming, pages 36 - 47, Paris, France, September 1999.
How to look busy while being as lazy as ever: the implementation of a lazy functional debugger
Henrik Nilsson. Journal of Functional Programming, 11(6):629 - 671, November 2001
Testing and Tracing Lazy Functional Programs Using QuickCheck and Hat
Koen Claessen, Colin Runciman, Olaf Chitil, and John Hughes. In Advanced Functional Programming: 4th International School, Lecture Notes in Computer Science, vol. 2638, pp. 59--99, Springer Verlag, 2002.
HsDebug: Debugging Lazy Programs by Not Being Lazy
Robert Ennals and Simon Peyton-Jones. Cambridge University, Microsoft Research.
Buddha: A Declarative Debugger for Haskell
By Bernie Pope.
Augmenting Trace-based Functional Debugging
Alastair Penney. PhD. Thesis. University of Bristol. September 1999.
Towards a theory of tracing for functional programs based on graph rewriting
Olaf Chitil and Yong Luo. In Ian Mackie, editor, Draft Proceedings of the 3rd International Workshop on Term Graph Rewriting, Termgraph 2006, page 10, April 2006.
A semantics for tracing. Olaf Chitil
In Thomas Arts and Markus Mohnen, editors, Draft Proceedings of the 13th International Workshop on Implementation of Functional Languages, IFL 2001, pages 249-254, lvsj, Sweden, September 2001. Ericsson Computer Science Laboratory.

[edit] 2 Testing

Testing Monadic Programs with QuickCheck
Koen Claessen, John Hughes. SIGPLAN Notices 37(12): 47-59 (2002)
QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs
Koen Claessen and John Hughes. In Proc. of International Conference on Functional Programming (ICFP), ACM SIGPLAN, 2000.
Specification Based Testing with QuickCheck
Koen Claessen and John Hughes. In Jeremy Gibbons and Oege de Moor (eds.), The Fun of Programming, Cornerstones of Computing, pp. 17--40, Palgrave, 2003.
QuickCheck: Specification-based Random Testing
Koen Claessen. Presentation at Summer Institute on Trends in Testing: Theory, Techniques and Tools, August 2004.
Testing Implementations of Formally Verified Algorithms
Thomas Arts, Koen Claessen, John Hughes, and Hans Svensson. In Proc. of Conference on Software Engineering Research and Practice (SERPS), Mlardalen University, October 2005.
Unit Testing with HUnit
Dean Herington. 2002.
Lazy assertions
Olaf Chitil, Dan McNeill, and Colin Runciman. In Draft Proceedings of the 15th International Workshop on Implementation of Functional Languages, IFL 2003, pages 31-46, Edinburgh, Scotland, September 2003.]
Testing Telecoms Software with Quviq QuickCheck
Thomas Arts, John Hughes, Joakim Johansson, Ulf Wiger, Proceedings of the Fifth ACM SIGPLAN Erlang Workshop - 2006

[edit] 3 Verifying Haskell programs

Static contract checking for Haskell
Dana Xu and Simon Peyton Jones, POPL 2009.
Formulating Haskell
Simon Thompson. Technical Report 29-92*, University of Kent, Computing Laboratory, University of Kent, Canterbury, UK, November 1992.
Verifying Haskell Programs by Combining Testing and Proving
By Peter Dybjer, Qiao Haiyan and Makoto Takeyama. Proceedings 3rd International Conference on Quality Software, IEEE Computer Society Press, pp. 272-279.
Verifying Haskell Programs Using Constructive Type Theory
Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell. Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, Tallinn, Estonia 62-73, 2005, ISBN 1-59593-071-X
Putting Curry-Howard to Work
Tim Sheard, Proceedings of the 2005 ACM SIGPLAN workshop on Haskell. Tallinn, Estonia, 74 - 85, 2005 ISBN 1-59593-071-X
Extended Static Checking for Haskell
Dana Xu, Haskell Workshop 2006
Unfailing Haskell: A static checker for pattern matching
Neil Mitchell, Colin Runciman, Trends in Functional Programming 2005.
Algebraic methods for optimization problems
Richard Bird, Jeremy Gibbons, and Shin Cheng Mu. In Roland Backhouse, Roy Crole, and Jeremy Gibbons, editors, Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, volume 2297 of Lecture Notes in Computer Science, pages 281-307. Springer-Verlag, 2002.
Proof-directed debugging: revisited
Kwangkeun Yi. JFP. 16(6):663-670
Language-Based Program Verification via Expressive Types
Martin Sulzmann and Razvan Voicu. In Programming Languages meet Program Verification (PLPV'06)
Proving Correctness via Free Theorems: The Case of the destroy/build-Rule
Janis Voigtländer. Workshop on Partial Evaluation and Program Manipulation (PEPM'08), Proceedings, ACM Press, 2008.


[edit] 3.1 Security

Flexible Dynamic Information Flow Control in Haskell
Deian Stefan, Alejandro Russo, John Mitchell, and David Mazieres.
Secure Multi-Execution in Haskell
Mauro Jaskelioff, Alejandro Russo.
A Library for Light-weight Information-Flow Security in Haskell
Alejandro Russo, Koen Claessen, John Hughes.
A Library for Secure Multi-threaded Information Flow in Haskell
Ta-chung Tsai, Alejandro Russo, John Hughes.
Encoding Information Flow in Haskell
Arrows for Secure Information Flow

See also work on verifying microkernels in Haskell

[edit] 4 Software reliability

Typed Contracts for Functional Programming
Ralf Hinze, Johan Jeuring and Andres Lh. In Philip Wadler and Masimi Hagiya, editors, Proceedings of the Eighth International Symposium on Functional and Logic Programming (FLOPS 2006), 24-26 April 2006, Fuji Susono, Japan.