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 @INPROCEEDINGS{Hydra,
277 author = {John O'Donnell},
278 title = {{From Transistors to Computer Architecture: Teaching Functional Circuit
279 Specification in Hydra}},
280 booktitle = {{Proceedings of the First International Symposium on Funtional Programming
281 Languages in Education}},
284 series = {Lecture Notes in Computer Science},
286 publisher = {Springer-Verlag},
288 timestamp = {2010.01.21}
292 author = {Ingo Sander and Axel Jantsch},
293 title = {{System Modeling and Transformational Design Refinement in ForSyDe}},
294 journal = {{IEEE Transactions on Computer-Aided Design of Integrated Circuits
303 timestamp = {2010.01.21}
306 @INPROCEEDINGS{ForSyDe1,
307 author = {Sander, Ingo and Jantsch, Axel},
308 title = {{Transformation based communication and clock domain refinement for
310 booktitle = {{DAC '02: Proceedings of the 39th annual Design Automation Conference}},
313 address = {New York, NY, USA},
315 doi = {http://doi.acm.org/10.1145/513918.513992},
316 isbn = {1-58113-461-4},
317 location = {New Orleans, Louisiana, USA},
319 timestamp = {2010.01.20}
322 @INPROCEEDINGS{T-Ruby,
323 author = {Sharp, Robin and Rasmussen, Ole},
324 title = {{Using a language of functions and relations for VLSI specification}},
325 booktitle = {FPCA '95: Proceedings of the seventh international conference on
326 Functional programming languages and computer architecture},
329 address = {New York, NY, USA},
331 doi = {http://doi.acm.org/10.1145/224164.224180},
332 isbn = {0-89791-719-7},
333 location = {La Jolla, California, United States},
335 timestamp = {2010.01.21}
339 author = {Sheeran, Mary},
340 title = {{$\mu$FP, a language for VLSI design}},
341 booktitle = {{LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional
345 address = {New York, NY, USA},
347 doi = {http://doi.acm.org/10.1145/800055.802026},
348 isbn = {0-89791-142-3},
349 location = {Austin, Texas, United States},
351 timestamp = {2010.01.20}
355 author = {Strachey, Christopher},
356 title = {Fundamental Concepts in Programming Languages},
357 howpublished = {Lecture Notes, International Summer School in Computer Programming,
361 note = {Reprinted in {\em Higher-Order and Symbolic Computation}, 13(1/2),
364 timestamp = {2010.02.24}
367 @INPROCEEDINGS{Sulzmann2007,
368 author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton
369 and Donnelly, Kevin},
370 title = {{System F with Type Equality Coercions}},
371 booktitle = {{TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop
372 on Types in languages design and implementation, Nice, France}},
375 address = {{New York, NY, USA}},
378 doi = {http://doi.acm.org/10.1145/1190315.1190324},
379 isbn = {1-59593-393-X},
380 location = {Nice, Nice, France},
382 timestamp = {2009.10.23}
386 author = {{The GHC Team}},
387 title = {{The Glasgow Haskell Compiler}},
388 url = {http://www.haskell.org/ghc/},
390 timestamp = {2010.02.25}
394 title = {{Haskell 98 language and libraries}},
396 editor = {Simon Peyton Jones},
400 series = {{Journal of Functional Programming}},
401 booktitle = {{Journal of Functional Programming}},
402 journal = {Journal of Functional Programming},
404 timestamp = {2010.01.29}
408 title = {{VHDL Language Reference Manual}},
409 organization = {IEEE},
410 number = {1076-2008},
413 timestamp = {2009.11.17}
417 title = {{Verilog Hardware Description Languages}},
418 organization = {{IEEE}},
419 number = {1365-2005},
422 timestamp = {2010.01.29}
425 @comment{jabref-meta: selector_publisher:}
427 @comment{jabref-meta: selector_author:}
429 @comment{jabref-meta: selector_journal:}
431 @comment{jabref-meta: selector_keywords:}