Difference between revisions of "Research papers/Domain specific languages"

From HaskellWiki
Jump to navigation Jump to search
(+papers)
(+papers)
Line 15: Line 15:
 
:J. Peterson, P. Hudak, A. Reid and G. Hager. In Proceedings of Third International Symposium on Practical Applications of Declarative Languages PADL'01, March 2001.
 
:J. Peterson, P. Hudak, A. Reid and G. Hager. In Proceedings of Third International Symposium on Practical Applications of Declarative Languages PADL'01, March 2001.
   
===Hardware description===
+
===Hardware design===
   
;[http://www.cs.chalmers.se/~koen/Papers/lava.ps Lava: Hardware Design in Haskell]
+
;[http://www.cs.chalmers.se/~koen/pubs/charme01-sorter.pdf The Design and Verification of a Sorter Core]
:Per Bjesse, Koen Claessen, Mary Sheeran, Satnam Singh
+
:Koen Claessen, Mary Sheeran, and Satnam Singh. In Proc. of Conference on Correct Hardware Design and Verification Methods (CHARME), Lecture Notes in Computer Science, Springer Verlag, 2001.
   
 
;[http://www.cs.chalmers.se/~koen/Papers/lic.ps An Embedded Language Approach to Hardware Description and Verification]
 
;[http://www.cs.chalmers.se/~koen/Papers/lic.ps An Embedded Language Approach to Hardware Description and Verification]
 
:Koen Claessen. Dept. of Computer Science and Engineering, Chalmers University of Technology, Lic. thesis, August 2000.
 
:Koen Claessen. Dept. of Computer Science and Engineering, Chalmers University of Technology, Lic. thesis, August 2000.
 
;[http://www.cs.chalmers.se/~koen/pubs/charme01-sorter.pdf The Design and Verification of a Sorter Core]
 
:Koen Claessen, Mary Sheeran, and Satnam Singh. In Proc. of Conference on Correct Hardware Design and Verification Methods (CHARME), Lecture Notes in Computer Science, Springer Verlag, 2001.
 
   
 
;[http://www.cs.chalmers.se/~koen/pubs/phd01-thesis.ps Embedded Languages for Describing and Verifying Hardware]
 
;[http://www.cs.chalmers.se/~koen/pubs/phd01-thesis.ps Embedded Languages for Describing and Verifying Hardware]
Line 31: Line 28:
 
;[http://www.cs.chalmers.se/~koen/pubs/fdpe02-lava.ps An Embedded Language Approach to Teaching Hardware Compilation]
 
;[http://www.cs.chalmers.se/~koen/pubs/fdpe02-lava.ps An Embedded Language Approach to Teaching Hardware Compilation]
 
:Koen Claessen and Gordon Pace. In Proc. of Workshop on Functional and Declarative Programming in Education (FDPE), 2002.
 
:Koen Claessen and Gordon Pace. In Proc. of Workshop on Functional and Declarative Programming in Education (FDPE), 2002.
  +
 
;[http://www.cs.chalmers.se/~koen/Papers/constructive.ps Safety Property Verification of Cyclic Circuits]
  +
:Koen Claessen. June 2002.
  +
  +
;[http://www.cs.chalmers.se/~koen/Papers/paps.ps Verification of Hardware Systems with First-Order Logic]
  +
:Koen Claessen, Reiner Hähnle, Johan Mårtensson. PaPS 2002. 2002.
  +
  +
;[http://www.cs.chalmers.se/~koen/Papers/dcc-hwcomp.ps An Embedded Language Framework for Hardware Compilation]
  +
:Koen Claessen, Gordon Pace. DCC 2002. 2002.
  +
  +
;[http://www.cs.chalmers.se/~koen/Papers/obs-shar.ps Observable Sharing for Functional Circuit Description]
  +
:Koen Claessen and David Sands. ASIAN '99. 1999.
  +
  +
;[http://www.cs.chalmers.se/~bjesse/fftpaper.ps.gz Automatic Verification of Combinational and Pipelined FFT Circuits]
  +
:Per Bjesse. CAV. 1999
  +
  +
;[http://www.cse.ogi.edu/PacSoft/publications/2000/phd-thesis-matthews.pdf Algebraic Specification and Verification of Processor Microarchitectures]
  +
:John Matthews. PhD. Thesis. Oregon Graduate Institute. 2000.
  +
  +
;[http://www.cse.ogi.edu/PacSoft/publications/1998/day.pdf Symbolic Simulation of Microprocessor Models using Type Classes in Haskell]
  +
:Nancy A. Day, Jeffrey R. Lewis and Byron Cook. CHARME'99. September 1999.
  +
  +
;[http://www.cse.ogi.edu/PacSoft/publications/phaseiiiq9papers/hawk.pdf On Embedding a Microarchitectural Design Language within Haskell]
  +
:John Launchbury, Jeff Lewis and Byron Cook. ICFP'99. 1999.
  +
  +
;[http://www.cse.ogi.edu/PacSoft/publications/phaseiiiq9papers/algebra.pdf Elementary Microarchitecture Algebra]
  +
:John Matthews and John Launchbury. CAV '99. 1999.
  +
  +
;[http://www.cse.ogi.edu/PacSoft/publications/1998/super.pdf Specifying Superscalar Microprocessors with Hawk]
  +
:Byron Cook, John Launchbury and John Matthews. FTH '98. 1998.
  +
  +
;[http://www.cse.ogi.edu/PacSoft/publications/1998/hawkIntro.pdf Microprocessor Specification in Hawk]
  +
:John Matthews, John Launchbury and Byron Cook. ICCL '98. 1998.
  +
  +
====Lava====
  +
  +
;[http://www.cs.chalmers.se/~koen/Papers/lava.ps Lava: Hardware Design in Haskell]
  +
:Per Bjesse, Koen Claessen, Mary Sheeran, Satnam Singh
   
 
;[http://www.math.chalmers.se/~koen/pubs/entry-sttt03-lava.html Using Lava to Design and Verify Recursive and Periodic Sorters]
 
;[http://www.math.chalmers.se/~koen/pubs/entry-sttt03-lava.html Using Lava to Design and Verify Recursive and Periodic Sorters]
Line 37: Line 72:
 
;[http://www.math.chalmers.se/~koen/pubs/entry-fop-lava.html Functional Hardware Description in Lava]
 
;[http://www.math.chalmers.se/~koen/pubs/entry-fop-lava.html Functional Hardware Description in Lava]
 
:Koen Claessen, Mary Sheeran, and Satnam Singh. In Jeremy Gibbons and Oege de Moor (eds.), The Fun of Programming, Cornerstones of Computing, pp. 151--176, Palgrave, 2003.
 
:Koen Claessen, Mary Sheeran, and Satnam Singh. In Jeremy Gibbons and Oege de Moor (eds.), The Fun of Programming, Cornerstones of Computing, pp. 151--176, Palgrave, 2003.
  +
  +
;[http://www.cs.chalmers.se/~koen/Lava/tutorial.ps A Lava Tutorial]
  +
:Koen Claessen, Mary Sheeran. April 2000.
   
 
===Logic programming===
 
===Logic programming===
Line 42: Line 80:
 
;[http://www.cs.chalmers.se/~koen/pubs/haskell00-typedlp.ps Typed Logical Variables in Haskell]
 
;[http://www.cs.chalmers.se/~koen/pubs/haskell00-typedlp.ps Typed Logical Variables in Haskell]
 
:Koen Claessen and Peter Ljunglöf. In Proc. of Haskell Workshop, ACM SIGPLAN, 2000. 1999
 
:Koen Claessen and Peter Ljunglöf. In Proc. of Haskell Workshop, ACM SIGPLAN, 2000. 1999
  +
  +
;[http://www.informatik.uni-bonn.de/~ralf/publications/Prolog.ps.gz Prolog's control constructs in a functional setting - Axioms and implementation]
  +
:Ralf Hinze. International Journal of Foundations of Computer Science. 12 (2). 2001.

Revision as of 02:47, 13 April 2006

Domain specific languages

Domain Specific Embedded Compilers
Daan Leijen and Erik Meijer. 2nd USENIX Conference on Domain-Specific Languages (DSL'99), Austin, Texas, October 1999. Also appeared in ACM SIGPLAN Notices 35, 1, January 2000.

Rapid prototyping

Prototyping Real-Time Vision Systems: An Experiment in DSL Design
A. Reid, J. Peterson, G. Hager and P. Hudak, In Proceedings of International Conference on Software Engineering (ICSE'99), Los Angeles, CA. 16-22 May, 1999.
FVision: A Declarative Language for Visual Tracking
J. Peterson, P. Hudak, A. Reid and G. Hager. In Proceedings of Third International Symposium on Practical Applications of Declarative Languages PADL'01, March 2001.

Hardware design

The Design and Verification of a Sorter Core
Koen Claessen, Mary Sheeran, and Satnam Singh. In Proc. of Conference on Correct Hardware Design and Verification Methods (CHARME), Lecture Notes in Computer Science, Springer Verlag, 2001.
An Embedded Language Approach to Hardware Description and Verification
Koen Claessen. Dept. of Computer Science and Engineering, Chalmers University of Technology, Lic. thesis, August 2000.
Embedded Languages for Describing and Verifying Hardware
Koen Claessen. Dept. of Computer Science and Engineering, Chalmers University of Technology, Ph.D. thesis, April 2001.
An Embedded Language Approach to Teaching Hardware Compilation
Koen Claessen and Gordon Pace. In Proc. of Workshop on Functional and Declarative Programming in Education (FDPE), 2002.
Safety Property Verification of Cyclic Circuits
Koen Claessen. June 2002.
Verification of Hardware Systems with First-Order Logic
Koen Claessen, Reiner Hähnle, Johan Mårtensson. PaPS 2002. 2002.
An Embedded Language Framework for Hardware Compilation
Koen Claessen, Gordon Pace. DCC 2002. 2002.
Observable Sharing for Functional Circuit Description
Koen Claessen and David Sands. ASIAN '99. 1999.
Automatic Verification of Combinational and Pipelined FFT Circuits
Per Bjesse. CAV. 1999
Algebraic Specification and Verification of Processor Microarchitectures
John Matthews. PhD. Thesis. Oregon Graduate Institute. 2000.
Symbolic Simulation of Microprocessor Models using Type Classes in Haskell
Nancy A. Day, Jeffrey R. Lewis and Byron Cook. CHARME'99. September 1999.
On Embedding a Microarchitectural Design Language within Haskell
John Launchbury, Jeff Lewis and Byron Cook. ICFP'99. 1999.
Elementary Microarchitecture Algebra
John Matthews and John Launchbury. CAV '99. 1999.
Specifying Superscalar Microprocessors with Hawk
Byron Cook, John Launchbury and John Matthews. FTH '98. 1998.
Microprocessor Specification in Hawk
John Matthews, John Launchbury and Byron Cook. ICCL '98. 1998.

Lava

Lava: Hardware Design in Haskell
Per Bjesse, Koen Claessen, Mary Sheeran, Satnam Singh
Using Lava to Design and Verify Recursive and Periodic Sorters
Koen Claessen, Mary Sheeran, and Satnam Singh. In International Journal on Software Tools for Technology Transfer, vol. 4 (3), pp. 349--358, Springer Verlag, 2003.
Functional Hardware Description in Lava
Koen Claessen, Mary Sheeran, and Satnam Singh. In Jeremy Gibbons and Oege de Moor (eds.), The Fun of Programming, Cornerstones of Computing, pp. 151--176, Palgrave, 2003.
A Lava Tutorial
Koen Claessen, Mary Sheeran. April 2000.

Logic programming

Typed Logical Variables in Haskell
Koen Claessen and Peter Ljunglöf. In Proc. of Haskell Workshop, ACM SIGPLAN, 2000. 1999
Prolog's control constructs in a functional setting - Axioms and implementation
Ralf Hinze. International Journal of Foundations of Computer Science. 12 (2). 2001.