1 % This file was created with JabRef 2.5.
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
11 series = {{Lecture Notes in Computer Science}},
13 publisher = {Springer Verlag},
15 timestamp = {2010.01.21}
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}},
25 address = {New York, NY, USA},
27 doi = {http://doi.acm.org/10.1145/289423.289440},
28 isbn = {1-58113-024-4},
29 location = {Baltimore, Maryland, United States},
31 timestamp = {2010.01.20}
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}},
41 timestamp = {2010.01.25}
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}},
50 timestamp = {2010.01.20}
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},
60 address = {Los Alamitos},
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.},
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},
85 official_url = {http://dx.doi.org/10.1109/DSD.2009.141},
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}
96 author = {Grundy,Jim and Melham,Tom and O'Leary,John},
97 title = {{A reflective functional language for hardware design and theorem
99 journal = {Journal of Functional Programming},
104 doi = {10.1017/S0956796805005757},
106 timestamp = {2010.01.21}
109 @BOOK{lambdacalculus,
110 title = {{The Lambda Calculus: its Syntax and Semantics}},
111 publisher = {{Elsevier Science}},
113 author = {{H.P. Barendregt}},
115 series = {{Studies in Logic and the Foundations of Mathematics}},
116 edition = {{Revised}},
118 timestamp = {2010.03.02}
121 @INPROCEEDINGS{DAISY,
122 author = {Johnson, Steven D.},
123 title = {Applicative programming and digital design},
124 booktitle = {POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on
125 Principles of programming languages},
128 address = {New York, NY, USA},
130 doi = {http://doi.acm.org/10.1145/800017.800533},
131 isbn = {0-89791-125-3},
132 location = {Salt Lake City, Utah, United States},
134 timestamp = {2010.01.25}
138 author = {Jones, G. and Sheeran, M.},
139 title = {{Circuit Design in Ruby}},
140 booktitle = {{Formal Methods for VLSI Design}},
142 address = {Lyngby, Denmark},
143 publisher = {Elsevier Science Publishers},
144 citeulike-article-id = {304676},
145 journal = {Circuit Design in Ruby},
146 keywords = {jones90},
148 posted-at = {2005-08-26 18:08:07},
150 timestamp = {2010.01.20}
154 author = {Yanbing Li and Leeser, M.},
155 title = {{HML, a novel hardware description language and its translation to
157 journal = {{Very Large Scale Integration (VLSI) Systems, IEEE Transactions on}},
163 doi = {10.1109/92.820756},
165 keywords = {ML language, hardware description languages, type theoryHML, SML functional
166 programming language, VHDL translation, digital design, hardware
167 description language, polymorphic type, translator, type checker,
170 timestamp = {2010.01.20}
174 author = {Yanbing Li and Leeser, M.},
175 title = {{HML: an innovative hardware description language and its translation
177 booktitle = {{Design Automation Conference, 1995. Proceedings of the ASP-DAC '95/CHDL
178 '95/VLSI '95., IFIP International Conference on Hardware Description
179 Languages; IFIP International Conference on Very Large Scale Integration.,
180 Asian and South Pacific}},
184 doi = {10.1109/ASPDAC.1995.486388},
185 keywords = {abstract data types, functional languages, functional programming,
186 hardware description languagesHML, VHDL, advanced type checking,
187 functional programming language, hardware description language, polymorphic
188 types, type inference},
190 timestamp = {2010.01.20}
194 author = {{Mark D. Aagaard and Robert B. Jones and Carl-Johan H. Seger}},
195 title = {{Lifted-FL: A Pragmatic Implementation of Combined Model Checking
196 and Theorem Proving}},
197 booktitle = {{Proceedings of 12th International Conference on Theorem Proving
198 in Higher Order Logics}},
203 publisher = {Springer Verlag},
205 timestamp = {2010.01.26}
208 @INPROCEEDINGS{Hawk1,
209 author = {Matthews, J. and Cook, B. and Launchbury, J.},
210 title = {{Microprocessor specification in Hawk}},
211 booktitle = {{Proceedings of 1998 International Conference on Computer Languages}},
215 abstract = {Modern microprocessors require an immense investment of time and effort
216 to create and verify, from the high level architectural design downwards.
217 We are exploring ways to increase the productivity of design engineers
218 by creating a domain specific language for specifying and simulating
219 processor architectures. We believe that the structuring principles
220 used in modern functional programming languages, such as static typing,
221 parametric polymorphism, first class functions, and lazy evaluation
222 provide a good formalism for such a domain specific language, and
223 have made initial progress by creating a library on top of the functional
224 language Haskell. We have specified the integer subset of an out
225 of order, superscalar DLX microprocessor, with register renaming,
226 a reorder buffer, a global reservation station, multiple execution
227 units, and speculative branch execution. Two key abstractions of
228 this library are the signal abstract data type (ADT), which models
229 the simulation history of a wire, and the transaction ADT, which
230 models the state of an entire instruction as it travels through the
232 doi = {10.1109/ICCL.1998.674160},
234 keywords = {abstract data types, formal specification, functional languages, functional
235 programming, hardware description languages, microprocessor chips,
236 software librariesHawk language, design engineers, domain specific
237 language, first class functions, functional language Haskell, functional
238 programming languages, global reservation station, high level architectural
239 design, integer subset, lazy evaluation, microprocessor specification,
240 multiple execution units, out of order superscalar DLX microprocessor,
241 parametric polymorphism, processor architecture simulation, register
242 renaming, reorder buffer, signal abstract data type, simulation history,
243 software library, speculative branch execution, static typing,, structuring
244 principles, transaction ADT},
246 timestamp = {2010.01.20}
250 author = {Meshkinpour, F. and Ercegovac, M. D.},
251 title = {A functional language for description and design of digital systems:
252 sequential constructs},
253 booktitle = {DAC '85: Proceedings of the 22nd ACM/IEEE Design Automation Conference},
256 address = {New York, NY, USA},
258 doi = {http://doi.acm.org/10.1145/317825.317865},
259 isbn = {0-8186-0635-5},
260 location = {Las Vegas, Nevada, United States},
262 timestamp = {2010.01.25}
265 @INPROCEEDINGS{Hydra,
266 author = {John O'Donnell},
267 title = {{From Transistors to Computer Architecture: Teaching Functional Circuit
268 Specification in Hydra}},
269 booktitle = {{Proceedings of the First International Symposium on Funtional Programming
270 Languages in Education}},
273 series = {Lecture Notes in Computer Science},
275 publisher = {Springer-Verlag},
277 timestamp = {2010.01.21}
281 author = {Ingo Sander and Axel Jantsch},
282 title = {{System Modeling and Transformational Design Refinement in ForSyDe}},
283 journal = {{IEEE Transactions on Computer-Aided Design of Integrated Circuits
292 timestamp = {2010.01.21}
295 @INPROCEEDINGS{ForSyDe1,
296 author = {Sander, Ingo and Jantsch, Axel},
297 title = {{Transformation based communication and clock domain refinement for
299 booktitle = {{DAC '02: Proceedings of the 39th annual Design Automation Conference}},
302 address = {New York, NY, USA},
304 doi = {http://doi.acm.org/10.1145/513918.513992},
305 isbn = {1-58113-461-4},
306 location = {New Orleans, Louisiana, USA},
308 timestamp = {2010.01.20}
311 @INPROCEEDINGS{T-Ruby,
312 author = {Sharp, Robin and Rasmussen, Ole},
313 title = {{Using a language of functions and relations for VLSI specification}},
314 booktitle = {FPCA '95: Proceedings of the seventh international conference on
315 Functional programming languages and computer architecture},
318 address = {New York, NY, USA},
320 doi = {http://doi.acm.org/10.1145/224164.224180},
321 isbn = {0-89791-719-7},
322 location = {La Jolla, California, United States},
324 timestamp = {2010.01.21}
328 author = {Sheeran, Mary},
329 title = {{$\mu$FP, a language for VLSI design}},
330 booktitle = {{LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional
334 address = {New York, NY, USA},
336 doi = {http://doi.acm.org/10.1145/800055.802026},
337 isbn = {0-89791-142-3},
338 location = {Austin, Texas, United States},
340 timestamp = {2010.01.20}
344 author = {Strachey, Christopher},
345 title = {Fundamental Concepts in Programming Languages},
346 howpublished = {Lecture Notes, International Summer School in Computer Programming,
350 note = {Reprinted in {\em Higher-Order and Symbolic Computation}, 13(1/2),
353 timestamp = {2010.02.24}
356 @INPROCEEDINGS{Sulzmann2007,
357 author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton
358 and Donnelly, Kevin},
359 title = {{System F with Type Equality Coercions}},
360 booktitle = {{TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop
361 on Types in languages design and implementation, Nice, France}},
364 address = {{New York, NY, USA}},
367 doi = {http://doi.acm.org/10.1145/1190315.1190324},
368 isbn = {1-59593-393-X},
369 location = {Nice, Nice, France},
371 timestamp = {2009.10.23}
375 author = {{The GHC Team}},
376 title = {{The Glasgow Haskell Compiler}},
377 url = {http://www.haskell.org/ghc/},
379 timestamp = {2010.02.25}
383 title = {{Haskell 98 language and libraries}},
385 editor = {Simon Peyton Jones},
389 series = {{Journal of Functional Programming}},
390 booktitle = {{Journal of Functional Programming}},
391 journal = {Journal of Functional Programming},
393 timestamp = {2010.01.29}
397 title = {{VHDL Language Reference Manual}},
398 organization = {IEEE},
399 number = {1076-2008},
402 timestamp = {2009.11.17}
406 title = {{Verilog Hardware Description Languages}},
407 organization = {{IEEE}},
408 number = {1365-2005},
411 timestamp = {2010.01.29}
414 @comment{jabref-meta: selector_publisher:}
416 @comment{jabref-meta: selector_author:}
418 @comment{jabref-meta: selector_journal:}
420 @comment{jabref-meta: selector_keywords:}