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},
155 title = {{HML: An Innovative Hardware Description Language and Its Translation
157 school = {Cornell University},
161 timestamp = {2010.03.08}
165 author = {Yanbing Li and Leeser, M.},
166 title = {{HML, a novel hardware description language and its translation to
168 journal = {{Very Large Scale Integration (VLSI) Systems, IEEE Transactions on}},
174 doi = {10.1109/92.820756},
176 keywords = {ML language, hardware description languages, type theoryHML, SML functional
177 programming language, VHDL translation, digital design, hardware
178 description language, polymorphic type, translator, type checker,
181 timestamp = {2010.01.20}
185 author = {Yanbing Li and Leeser, M.},
186 title = {{HML: an innovative hardware description language and its translation
188 booktitle = {{Design Automation Conference, 1995. Proceedings of the ASP-DAC '95/CHDL
189 '95/VLSI '95., IFIP International Conference on Hardware Description
190 Languages; IFIP International Conference on Very Large Scale Integration.,
191 Asian and South Pacific}},
195 doi = {10.1109/ASPDAC.1995.486388},
196 keywords = {abstract data types, functional languages, functional programming,
197 hardware description languagesHML, VHDL, advanced type checking,
198 functional programming language, hardware description language, polymorphic
199 types, type inference},
201 timestamp = {2010.01.20}
205 author = {{Mark D. Aagaard and Robert B. Jones and Carl-Johan H. Seger}},
206 title = {{Lifted-FL: A Pragmatic Implementation of Combined Model Checking
207 and Theorem Proving}},
208 booktitle = {{Proceedings of 12th International Conference on Theorem Proving
209 in Higher Order Logics}},
214 publisher = {Springer Verlag},
216 timestamp = {2010.01.26}
219 @INPROCEEDINGS{Hawk1,
220 author = {Matthews, J. and Cook, B. and Launchbury, J.},
221 title = {{Microprocessor specification in Hawk}},
222 booktitle = {{Proceedings of 1998 International Conference on Computer Languages}},
226 abstract = {Modern microprocessors require an immense investment of time and effort
227 to create and verify, from the high level architectural design downwards.
228 We are exploring ways to increase the productivity of design engineers
229 by creating a domain specific language for specifying and simulating
230 processor architectures. We believe that the structuring principles
231 used in modern functional programming languages, such as static typing,
232 parametric polymorphism, first class functions, and lazy evaluation
233 provide a good formalism for such a domain specific language, and
234 have made initial progress by creating a library on top of the functional
235 language Haskell. We have specified the integer subset of an out
236 of order, superscalar DLX microprocessor, with register renaming,
237 a reorder buffer, a global reservation station, multiple execution
238 units, and speculative branch execution. Two key abstractions of
239 this library are the signal abstract data type (ADT), which models
240 the simulation history of a wire, and the transaction ADT, which
241 models the state of an entire instruction as it travels through the
243 doi = {10.1109/ICCL.1998.674160},
245 keywords = {abstract data types, formal specification, functional languages, functional
246 programming, hardware description languages, microprocessor chips,
247 software librariesHawk language, design engineers, domain specific
248 language, first class functions, functional language Haskell, functional
249 programming languages, global reservation station, high level architectural
250 design, integer subset, lazy evaluation, microprocessor specification,
251 multiple execution units, out of order superscalar DLX microprocessor,
252 parametric polymorphism, processor architecture simulation, register
253 renaming, reorder buffer, signal abstract data type, simulation history,
254 software library, speculative branch execution, static typing,, structuring
255 principles, transaction ADT},
257 timestamp = {2010.01.20}
261 author = {Meshkinpour, F. and Ercegovac, M. D.},
262 title = {A functional language for description and design of digital systems:
263 sequential constructs},
264 booktitle = {DAC '85: Proceedings of the 22nd ACM/IEEE Design Automation Conference},
267 address = {New York, NY, USA},
269 doi = {http://doi.acm.org/10.1145/317825.317865},
270 isbn = {0-8186-0635-5},
271 location = {Las Vegas, Nevada, United States},
273 timestamp = {2010.01.25}
276 @INCOLLECTION{Bluespec,
277 author = {Rishiyur S. Nikhil},
278 title = {{Bluespec: A General-Purpose Approach to High-Level Synthesis Based
279 on Parallel Atomic Transactions}},
280 booktitle = {{High-Level Synthesis - From Algorithm to Digital Circuit}},
281 publisher = {Springer Netherlands},
283 editor = {{Philippe Coussy and Adam Morawiec}},
286 timestamp = {2010.03.09}
289 @INPROCEEDINGS{Hydra,
290 author = {John O'Donnell},
291 title = {{From Transistors to Computer Architecture: Teaching Functional Circuit
292 Specification in Hydra}},
293 booktitle = {{Proceedings of the First International Symposium on Funtional Programming
294 Languages in Education}},
297 series = {Lecture Notes in Computer Science},
299 publisher = {Springer-Verlag},
301 timestamp = {2010.01.21}
305 author = {Ingo Sander and Axel Jantsch},
306 title = {{System Modeling and Transformational Design Refinement in ForSyDe}},
307 journal = {{IEEE Transactions on Computer-Aided Design of Integrated Circuits
316 timestamp = {2010.01.21}
319 @INPROCEEDINGS{ForSyDe1,
320 author = {Sander, Ingo and Jantsch, Axel},
321 title = {{Transformation based communication and clock domain refinement for
323 booktitle = {{DAC '02: Proceedings of the 39th annual Design Automation Conference}},
326 address = {New York, NY, USA},
328 doi = {http://doi.acm.org/10.1145/513918.513992},
329 isbn = {1-58113-461-4},
330 location = {New Orleans, Louisiana, USA},
332 timestamp = {2010.01.20}
335 @INPROCEEDINGS{T-Ruby,
336 author = {Sharp, Robin and Rasmussen, Ole},
337 title = {{Using a language of functions and relations for VLSI specification}},
338 booktitle = {FPCA '95: Proceedings of the seventh international conference on
339 Functional programming languages and computer architecture},
342 address = {New York, NY, USA},
344 doi = {http://doi.acm.org/10.1145/224164.224180},
345 isbn = {0-89791-719-7},
346 location = {La Jolla, California, United States},
348 timestamp = {2010.01.21}
352 author = {Sheeran, Mary},
353 title = {{$\mu$FP, a language for VLSI design}},
354 booktitle = {{LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional
358 address = {New York, NY, USA},
360 doi = {http://doi.acm.org/10.1145/800055.802026},
361 isbn = {0-89791-142-3},
362 location = {Austin, Texas, United States},
364 timestamp = {2010.01.20}
368 author = {Strachey, Christopher},
369 title = {Fundamental Concepts in Programming Languages},
370 howpublished = {Lecture Notes, International Summer School in Computer Programming,
374 note = {Reprinted in {\em Higher-Order and Symbolic Computation}, 13(1/2),
377 timestamp = {2010.02.24}
380 @INPROCEEDINGS{Sulzmann2007,
381 author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton
382 and Donnelly, Kevin},
383 title = {{System F with Type Equality Coercions}},
384 booktitle = {{TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop
385 on Types in languages design and implementation, Nice, France}},
388 address = {{New York, NY, USA}},
391 doi = {http://doi.acm.org/10.1145/1190315.1190324},
392 isbn = {1-59593-393-X},
393 location = {Nice, Nice, France},
395 timestamp = {2009.10.23}
399 author = {{The GHC Team}},
400 title = {{The Glasgow Haskell Compiler}},
401 url = {http://www.haskell.org/ghc/},
403 timestamp = {2010.02.25}
407 title = {{Haskell 98 language and libraries}},
409 editor = {Simon Peyton Jones},
413 series = {{Journal of Functional Programming}},
414 booktitle = {{Journal of Functional Programming}},
415 journal = {Journal of Functional Programming},
417 timestamp = {2010.01.29}
421 title = {{VHDL Language Reference Manual}},
422 organization = {IEEE},
423 number = {1076-2008},
426 timestamp = {2009.11.17}
430 title = {{Verilog Hardware Description Languages}},
431 organization = {{IEEE}},
432 number = {1365-2005},
435 timestamp = {2010.01.29}
438 @comment{jabref-meta: selector_publisher:}
440 @comment{jabref-meta: selector_author:}
442 @comment{jabref-meta: selector_journal:}
444 @comment{jabref-meta: selector_keywords:}