Update piece about state to show relation between the run function and the statefull...
[matthijs/master-project/dsd-paper.git] / clash.bib
1 % This file was created with JabRef 2.5.
2 % Encoding: MacRoman
3
4 @INPROCEEDINGS{Wired,
5   author = {Emil Axelsson and Koen Claessen and Mary Sheeran},
6   title = {{Wired: Wire-Aware Circuit Design}},
7   booktitle = {{Proceedings of Conference on Correct Hardware Design and VeriÞcation
8         Methods (CHARME)}},
9   year = {2005},
10   volume = {3725},
11   series = {{Lecture Notes in Computer Science}},
12   pages = {{5--19}},
13   publisher = {Springer Verlag},
14   owner = {darchon},
15   timestamp = {2010.01.21}
16 }
17
18 @INPROCEEDINGS{Lava,
19   author = {Bjesse, Per and Claessen, Koen and Sheeran, Mary and Singh, Satnam},
20   title = {{Lava: hardware design in Haskell}},
21   booktitle = {{ICFP '98: Proceedings of the third ACM SIGPLAN international conference
22         on Functional programming}},
23   year = {1998},
24   pages = {174--184},
25   address = {New York, NY, USA},
26   publisher = {ACM},
27   doi = {http://doi.acm.org/10.1145/289423.289440},
28   isbn = {1-58113-024-4},
29   location = {Baltimore, Maryland, United States},
30   owner = {darchon},
31   timestamp = {2010.01.20}
32 }
33
34 @INPROCEEDINGS{Cardelli1981,
35   author = {Luca Cardelli and Gordon Plotkin},
36   title = {{An Algebraic Approach to VLSI Design}},
37   booktitle = {{Proceedings of the VLSI 81 International Conference}},
38   year = {1981},
39   pages = {173-182},
40   owner = {darchon},
41   timestamp = {2010.01.25}
42 }
43
44 @INPROCEEDINGS{Hawk2,
45   author = {Byron Cook and John Launchbury and John Matthews},
46   title = {{Specifying superscalar microprocessors in Hawk}},
47   booktitle = {{Formal Techniques for Hardware and Hardware-like Systems}},
48   year = {1998},
49   owner = {darchon},
50   timestamp = {2010.01.20}
51 }
52
53 @INPROCEEDINGS{reductioncircuit,
54   author = {M. E. T. Gerards and J. Kuper and A. B. J. Kokkeler and E. Molenkamp},
55   title = {Streaming Reduction Circuit},
56   booktitle = {Proceedings of the 12th EUROMICRO Conference on Digital System Design,
57         Architectures, Methods and Tools, Patras, Greece},
58   year = {2009},
59   pages = {287--292},
60   address = {Los Alamitos},
61   month = {August},
62   publisher = {IEEE Computer Society Press},
63   abstract = {Reduction circuits are used to reduce rows of ?oating point values
64         to single values. Binary ?oating point operators often have deep
65         pipelines, which may cause hazards when many consecutive rows have
66         to be reduced. We present an algorithm by which any number of consecutive
67         rows of arbitrary lengths can be reduced by a pipelined commutative
68         and associative binary operator in an efficient manner. The algorithm
69         is simple to implement, has a low latency, produces results in-order,
70         and requires only small buffers. Besides, it uses only a single pipeline
71         for the involved operation. The complexity of the algorithm depends
72         on the depth of the pipeline, not on the length of the input rows.
73         In this paper we discuss an implementation of this algorithm and
74         we prove its correctness.},
75   eprintid = {17041},
76   event_dates = {27-29 Aug 2009},
77   event_type = {Conference},
78   howpublished = {http://eprints.eemcs.utwente.nl/17041/},
79   id_number = {10.1109/DSD.2009.141},
80   international = {Yes},
81   isbn_13 = {978-0-7695-3782-5},
82   ispublished = {Published},
83   location = {Patras, Greece},
84   num_pages = {6},
85   official_url = {http://dx.doi.org/10.1109/DSD.2009.141},
86   owner = {baaijcpr},
87   pres_types = {Talk},
88   refereed = {Yes},
89   research_groups = {EWI-CAES: Computer Architecture for Embedded Systems},
90   research_programs = {CTIT-WiSe: Wireless and Sensor Systems},
91   research_projects = {EASY: Embedded Adaptive Streaming sYstems},
92   timestamp = {2010.02.26}
93 }
94
95 @ARTICLE{reFLect,
96   author = {Grundy,Jim and Melham,Tom and O'Leary,John},
97   title = {{A reflective functional language for hardware design and theorem
98         proving}},
99   journal = {Journal of Functional Programming},
100   year = {2006},
101   volume = {16},
102   pages = {157-196},
103   number = {02},
104   doi = {10.1017/S0956796805005757},
105   owner = {darchon},
106   timestamp = {2010.01.21}
107 }
108
109 @INPROCEEDINGS{DAISY,
110   author = {Johnson, Steven D.},
111   title = {Applicative programming and digital design},
112   booktitle = {POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on
113         Principles of programming languages},
114   year = {1984},
115   pages = {218--227},
116   address = {New York, NY, USA},
117   publisher = {ACM},
118   doi = {http://doi.acm.org/10.1145/800017.800533},
119   isbn = {0-89791-125-3},
120   location = {Salt Lake City, Utah, United States},
121   owner = {darchon},
122   timestamp = {2010.01.25}
123 }
124
125 @INPROCEEDINGS{Ruby,
126   author = {Jones, G. and Sheeran, M.},
127   title = {{Circuit Design in Ruby}},
128   booktitle = {{Formal Methods for VLSI Design}},
129   year = {1990},
130   address = {Lyngby, Denmark},
131   publisher = {Elsevier Science Publishers},
132   citeulike-article-id = {304676},
133   journal = {Circuit Design in Ruby},
134   keywords = {jones90},
135   owner = {darchon},
136   posted-at = {2005-08-26 18:08:07},
137   priority = {0},
138   timestamp = {2010.01.20}
139 }
140
141 @ARTICLE{HML2,
142   author = {Yanbing Li and Leeser, M.},
143   title = {{HML, a novel hardware description language and its translation to
144         VHDL}},
145   journal = {{Very Large Scale Integration (VLSI) Systems, IEEE Transactions on}},
146   year = {2000},
147   volume = {8},
148   pages = {1-8},
149   number = {1},
150   month = {Feb},
151   doi = {10.1109/92.820756},
152   issn = {1063-8210},
153   keywords = {ML language, hardware description languages, type theoryHML, SML functional
154         programming language, VHDL translation, digital design, hardware
155         description language, polymorphic type, translator, type checker,
156         type inference},
157   owner = {darchon},
158   timestamp = {2010.01.20}
159 }
160
161 @INPROCEEDINGS{HML1,
162   author = {Yanbing Li and Leeser, M.},
163   title = {{HML: an innovative hardware description language and its translation
164         to VHDL}},
165   booktitle = {{Design Automation Conference, 1995. Proceedings of the ASP-DAC '95/CHDL
166         '95/VLSI '95., IFIP International Conference on Hardware Description
167         Languages; IFIP International Conference on Very Large Scale Integration.,
168         Asian and South Pacific}},
169   year = {1995},
170   pages = {691-696},
171   month = {Aug-1 Sep},
172   doi = {10.1109/ASPDAC.1995.486388},
173   keywords = {abstract data types, functional languages, functional programming,
174         hardware description languagesHML, VHDL, advanced type checking,
175         functional programming language, hardware description language, polymorphic
176         types, type inference},
177   owner = {darchon},
178   timestamp = {2010.01.20}
179 }
180
181 @INPROCEEDINGS{FL,
182   author = {{Mark D. Aagaard and Robert B. Jones and Carl-Johan H. Seger}},
183   title = {{Lifted-FL: A Pragmatic Implementation of Combined Model Checking
184         and Theorem Proving}},
185   booktitle = {{Proceedings of 12th International Conference on Theorem Proving
186         in Higher Order Logics}},
187   year = {1999},
188   volume = {1690},
189   series = {LNCS},
190   pages = {323-340},
191   publisher = {Springer Verlag},
192   owner = {darchon},
193   timestamp = {2010.01.26}
194 }
195
196 @INPROCEEDINGS{Hawk1,
197   author = {Matthews, J. and Cook, B. and Launchbury, J.},
198   title = {{Microprocessor specification in Hawk}},
199   booktitle = {{Proceedings of 1998 International Conference on Computer Languages}},
200   year = {1998},
201   pages = {90-101},
202   month = {May},
203   abstract = {Modern microprocessors require an immense investment of time and effort
204         to create and verify, from the high level architectural design downwards.
205         We are exploring ways to increase the productivity of design engineers
206         by creating a domain specific language for specifying and simulating
207         processor architectures. We believe that the structuring principles
208         used in modern functional programming languages, such as static typing,
209         parametric polymorphism, first class functions, and lazy evaluation
210         provide a good formalism for such a domain specific language, and
211         have made initial progress by creating a library on top of the functional
212         language Haskell. We have specified the integer subset of an out
213         of order, superscalar DLX microprocessor, with register renaming,
214         a reorder buffer, a global reservation station, multiple execution
215         units, and speculative branch execution. Two key abstractions of
216         this library are the signal abstract data type (ADT), which models
217         the simulation history of a wire, and the transaction ADT, which
218         models the state of an entire instruction as it travels through the
219         microprocessor},
220   doi = {10.1109/ICCL.1998.674160},
221   issn = {1074-8970},
222   keywords = {abstract data types, formal specification, functional languages, functional
223         programming, hardware description languages, microprocessor chips,
224         software librariesHawk language, design engineers, domain specific
225         language, first class functions, functional language Haskell, functional
226         programming languages, global reservation station, high level architectural
227         design, integer subset, lazy evaluation, microprocessor specification,
228         multiple execution units, out of order superscalar DLX microprocessor,
229         parametric polymorphism, processor architecture simulation, register
230         renaming, reorder buffer, signal abstract data type, simulation history,
231         software library, speculative branch execution, static typing,, structuring
232         principles, transaction ADT},
233   owner = {darchon},
234   timestamp = {2010.01.20}
235 }
236
237 @INPROCEEDINGS{FHDL,
238   author = {Meshkinpour, F. and Ercegovac, M. D.},
239   title = {A functional language for description and design of digital systems:
240         sequential constructs},
241   booktitle = {DAC '85: Proceedings of the 22nd ACM/IEEE Design Automation Conference},
242   year = {1985},
243   pages = {238--244},
244   address = {New York, NY, USA},
245   publisher = {ACM},
246   doi = {http://doi.acm.org/10.1145/317825.317865},
247   isbn = {0-8186-0635-5},
248   location = {Las Vegas, Nevada, United States},
249   owner = {darchon},
250   timestamp = {2010.01.25}
251 }
252
253 @INPROCEEDINGS{Hydra,
254   author = {John O'Donnell},
255   title = {{From Transistors to Computer Architecture: Teaching Functional Circuit
256         Specification in Hydra}},
257   booktitle = {{Proceedings of the First International Symposium on Funtional Programming
258         Languages in Education}},
259   year = {1995},
260   volume = {1022},
261   series = {Lecture Notes in Computer Science},
262   pages = {195--214},
263   publisher = {Springer-Verlag},
264   owner = {darchon},
265   timestamp = {2010.01.21}
266 }
267
268 @ARTICLE{ForSyDe2,
269   author = {Ingo Sander and Axel Jantsch},
270   title = {{System Modeling and Transformational Design Refinement in ForSyDe}},
271   journal = {{IEEE Transactions on Computer-Aided Design of Integrated Circuits
272         and Systems}},
273   year = {2004},
274   volume = {23},
275   pages = {17--32},
276   number = {1},
277   month = {January},
278   key = {ForSyDe},
279   owner = {darchon},
280   timestamp = {2010.01.21}
281 }
282
283 @INPROCEEDINGS{ForSyDe1,
284   author = {Sander, Ingo and Jantsch, Axel},
285   title = {{Transformation based communication and clock domain refinement for
286         system design}},
287   booktitle = {{DAC '02: Proceedings of the 39th annual Design Automation Conference}},
288   year = {2002},
289   pages = {281--286},
290   address = {New York, NY, USA},
291   publisher = {ACM},
292   doi = {http://doi.acm.org/10.1145/513918.513992},
293   isbn = {1-58113-461-4},
294   location = {New Orleans, Louisiana, USA},
295   owner = {darchon},
296   timestamp = {2010.01.20}
297 }
298
299 @INPROCEEDINGS{T-Ruby,
300   author = {Sharp, Robin and Rasmussen, Ole},
301   title = {{Using a language of functions and relations for VLSI specification}},
302   booktitle = {FPCA '95: Proceedings of the seventh international conference on
303         Functional programming languages and computer architecture},
304   year = {1995},
305   pages = {45--54},
306   address = {New York, NY, USA},
307   publisher = {ACM},
308   doi = {http://doi.acm.org/10.1145/224164.224180},
309   isbn = {0-89791-719-7},
310   location = {La Jolla, California, United States},
311   owner = {darchon},
312   timestamp = {2010.01.21}
313 }
314
315 @INPROCEEDINGS{muFP,
316   author = {Sheeran, Mary},
317   title = {{$\mu$FP, a language for VLSI design}},
318   booktitle = {{LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional
319         programming}},
320   year = {1984},
321   pages = {104--112},
322   address = {New York, NY, USA},
323   publisher = {ACM},
324   doi = {http://doi.acm.org/10.1145/800055.802026},
325   isbn = {0-89791-142-3},
326   location = {Austin, Texas, United States},
327   owner = {darchon},
328   timestamp = {2010.01.20}
329 }
330
331 @MISC{polymorphism,
332   author = {Strachey, Christopher},
333   title = {Fundamental Concepts in Programming Languages},
334   howpublished = {Lecture Notes, International Summer School in Computer Programming,
335         Copenhagen},
336   month = August,
337   year = {1967},
338   note = {Reprinted in {\em Higher-Order and Symbolic Computation}, 13(1/2),
339         pp. 1--49, 2000},
340   owner = {baaijcpr},
341   timestamp = {2010.02.24}
342 }
343
344 @INPROCEEDINGS{Sulzmann2007,
345   author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton
346         and Donnelly, Kevin},
347   title = {{System F with Type Equality Coercions}},
348   booktitle = {{TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop
349         on Types in languages design and implementation, Nice, France}},
350   year = {2007},
351   pages = {53--66},
352   address = {{New York, NY, USA}},
353   month = {January},
354   publisher = {{ACM}},
355   doi = {http://doi.acm.org/10.1145/1190315.1190324},
356   isbn = {1-59593-393-X},
357   location = {Nice, Nice, France},
358   owner = {darchon},
359   timestamp = {2009.10.23}
360 }
361
362 @ELECTRONIC{ghc,
363   author = {{The GHC Team}},
364   title = {{The Glasgow Haskell Compiler}},
365   url = {http://www.haskell.org/ghc/},
366   owner = {baaijcpr},
367   timestamp = {2010.02.25}
368 }
369
370 @BOOK{Haskell,
371   title = {{Haskell 98 language and libraries}},
372   year = {2003},
373   editor = {Simon Peyton Jones},
374   volume = {13},
375   number = {1},
376   pages = {1--255},
377   series = {{Journal of Functional Programming}},
378   booktitle = {{Journal of Functional Programming}},
379   journal = {Journal of Functional Programming},
380   owner = {darchon},
381   timestamp = {2010.01.29}
382 }
383
384 @STANDARD{VHDL2008,
385   title = {{VHDL Language Reference Manual}},
386   organization = {IEEE},
387   number = {1076-2008},
388   year = {2008},
389   owner = {darchon},
390   timestamp = {2009.11.17}
391 }
392
393 @STANDARD{Verilog,
394   title = {{Verilog Hardware Description Languages}},
395   organization = {{IEEE}},
396   number = {1365-2005},
397   year = {2005},
398   owner = {darchon},
399   timestamp = {2010.01.29}
400 }
401
402 @comment{jabref-meta: selector_publisher:}
403
404 @comment{jabref-meta: selector_author:}
405
406 @comment{jabref-meta: selector_journal:}
407
408 @comment{jabref-meta: selector_keywords:}
409