Research papers/Domain specific languages: Difference between revisions
DonStewart (talk | contribs) (+papers) |
DonStewart (talk | contribs) (+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 | ===Hardware design=== | ||
;[http://www.cs.chalmers.se/~koen/ | ;[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/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/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.