tutorial/literature.bib · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on de0bcbd help sign in

Idris-dev/tutorial/literature.bib

3856 lines 111 kB history raw

1@inproceedings{res-dsl-padl12,

2 title = {Resource-safe Systems Programming with Embedded Domain Specific Languages},

3 year = {2012},

4 booktitle = {Practical Applications of Declarative Languages 2012},

5 author = {Edwin Brady and Kevin Hammond},

6 series = {LNCS},

7 publisher = {Springer},

8 note = {To appear}

9}

11@article{lambdapi,

12 author = {Andres L\"{o}h and Conor McBride and Wouter Swierstra},

13 title = {A tutorial implementation of a dependently typed lambda calculus},

14 year = 2010,

15 journal = {Fundamenta Informaticae},

16 volume = 102,

17 number = 2

18}

20@article{idioms,

21 author = {McBride, Conor and Paterson, Ross},

22 title = {Applicative programming with effects},

23 journal = {J. Funct. Program.},

24 volume = {18},

25 issue = {1},

26 month = {January},

27 year = {2008},

28 issn = {0956-7968},

29 pages = {1--13},

30 numpages = {13},

31 url = {http://portal.acm.org/citation.cfm?id=1348940.1348941},

32 doi = {10.1017/S0956796807006326},

33 acmid = {1348941},

34 publisher = {Cambridge University Press},

35 address = {New York, NY, USA},

36}

38@inproceedings{lava,

39 author = {Bjesse, Per and Claessen, Koen and Sheeran, Mary and Singh, Satnam},

40 title = {Lava: hardware design in {Haskell}},

41 booktitle = {Proceedings of the third ACM SIGPLAN international conference on Functional programming},

42 series = {ICFP '98},

43 year = {1998},

44 isbn = {1-58113-024-4},

45 location = {Baltimore, Maryland, United States},

46 pages = {174--184},

47 numpages = {11},

48 url = {http://doi.acm.org/10.1145/289423.289440},

49 doi = {http://doi.acm.org/10.1145/289423.289440},

50 acmid = {289440},

51 publisher = {ACM},

52 address = {New York, NY, USA},

53}

55@inproceedings{plpv11,

56 author = {Edwin Brady},

57 title = {Idris --- Systems programming meets full dependent types},

58 booktitle = {Programming Languages meets Program Verification {(PLPV 2011)}},

59 year = {2011},

60 pages = {43--54},

61 ee = {http://doi.acm.org/10.1145/1929529.1929536},

62 bibsource = {DBLP, http://dblp.uni-trier.de}

65@inproceedings{epic-tfp,

66 author = {Edwin Brady},

67 title = {Epic --- a library for generating compilers},

68 year = 2011,

69 booktitle = {{Trends in Functional Programming} ({TFP} '11)},

70 note = {To appear}

73@inproceedings{ynot08,

74 author = {Nanevski,, Aleksandar and Morrisett,, Greg and

75 Shinnar,, Avraham and Govereau,, Paul and Birkedal,,

76 Lars},

77 title = {Ynot: reasoning with the awkward squad},

78 booktitle = {{ICFP} '08: Proceeding of the 13th {ACM SIGPLAN}

79 international conference on Functional programming},

80 year = {2008},

81 isbn = {978-1-59593-919-7},

82 pages = {229--240},

83 location = {Victoria, BC, Canada},

84 doi = {http://doi.acm.org/10.1145/1411204.1411237},

85 publisher = {ACM},

86 address = {New York, NY, USA},

89@article{cbconc-fi,

90 author = {Edwin Brady and Kevin Hammond},

91 title = {Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols},

92 year = 2010,

93 journal = {Fundamenta Informaticae},

94 volume = 102,

95 number = 2,

96 pages = {145--176}

97}

99@inproceedings{devil-osdi00,

100 author = {Fabrice M{\'e}rillon and

101 Laurent R{\'e}veill{\`e}re and

102 Charles Consel and

103 Renaud Marlet and

104 Gilles Muller},

105 title = {Devil: An IDL for Hardware Programming},

106 booktitle = {4th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2000)},

107 year = {2000}

111@INPROCEEDINGS{device-osdi08,

112 author = {Dan Williams and Patrick Reynolds and Kevin Walsh and Emin Gün Sirer and Fred B. Schneider},

113 title = {Device driver safety through a reference validation mechanism},

114 booktitle = {8th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008)},

115 year = {2008}

118@inproceedings{sozeau-equations,

119 author = {Matthieu Sozeau},

120 title = {Equations: A Dependent Pattern-Matching Compiler},

121 booktitle = {First International Conference on Interactive Theorem Proving (ITP 2010)},

122 year = {2010},

123 pages = {419--434},

124 ee = {http://dx.doi.org/10.1007/978-3-642-14052-5_29},

125 crossref = {DBLP:conf/itp/2010},

126 bibsource = {DBLP, http://dblp.uni-trier.de}

130@inproceedings{packet-type,

131 author = "Peter J. McCann and Satish Chandra",

132 title = "Packet Types: Abstract Specification of Network Protocol Messages",

133 year = 2000,

134 booktitle = "SIGCOMM '00",

135 publisher = {{ACM}}

138@inproceedings{qs-types,

139 author = {Eelis {van der Weegen} and James McKinna},

141 title={A Machine-checked Proof of the Average-case Complexity of Quicksort in Coq},

142 year={2009},

143 pages={256--271},

144 series = {Lecture Notes in Computer Science},

145 publisher = {Springer}

149@inproceedings{totalparser,

150 author = {Nils Anders Danielsson},

151 title = {Total Parser Combinators},

152 booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},

153 year = {2010},

154 isbn = {978-1-60558-794-3},

155 pages = {285--296},

156 location = {Baltimore, Maryland, USA},

157 doi = {http://doi.{ACM}.org/10.1145/1863543.1863587},

158 publisher = {{ACM}},

159 address = {New York, NY, USA},

162@misc{rfc791,

163 author="J. Postel",

164 title="{Internet Protocol}",

165 series="Request for Comments",

166 number="791",

167 howpublished="RFC 791 (Standard)",

168 publisher="IETF",

169 organization="Internet Engineering Task Force",

170 year=1981,

171 month=sep,

172 note="Updated by RFC 1349",

173 url="http://www.ietf.org/rfc/rfc791.txt",

177@misc{rfc792,

178 author="J. Postel",

179 title="{Internet Control Message Protocol}",

180 series="Request for Comments",

181 number="792",

182 howpublished="RFC 792 (Standard)",

183 publisher="IETF",

184 organization="Internet Engineering Task Force",

185 year=1981,

186 month=sep,

187 note="Updated by RFCs 950, 4884",

188 url="http://www.ietf.org/rfc/rfc792.txt",

191@INPROCEEDINGS{Dybjer-indrec,

192 author = {Peter Dybjer and Anton Setzer},

193 title = {A Finite Axiomatization of Inductive-Recursive Definitions},

194 booktitle = {Tyed Lambda Calculi and Applications},

195 volume = {1581},

196 series = {Lecture Notes in Computer Science},

197 year = {1998},

198 pages = {129--146},

199 publisher = {Springer}

202@book{stevenstcpip,

203 author = {W. Richard Stevens},

204 title = {{TCP/IP} Illustrated Volume 1: The Protocols},

205 year = 1994,

206 publisher = {Addison Wesley},

207 isbn = {0-201-63346-9}

210@inproceedings{coqtypeclasses,

211 author = {Sozeau, Matthieu and Oury, Nicolas},

212 title = {First-Class Type Classes},

213 booktitle = {TPHOLs '08: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics},

214 year = {2008},

215 isbn = {978-3-540-71065-3},

216 pages = {278--293},

217 location = {Montreal, P.Q., Canada},

218 doi = {http://dx.doi.org/10.1007/978-3-540-71067-7_23},

219 publisher = {Springer-Verlag},

220 address = {Berlin, Heidelberg},

224@inproceedings{kipling,

225 author = {McBride, Conor},

226 title = {Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation},

227 booktitle = {WGP '10: Proceedings of the 6th {ACM} {SIGPLAN} workshop on Generic programming},

228 year = {2010},

229 isbn = {978-1-4503-0251-7},

230 pages = {1--12},

231 location = {Baltimore, Maryland, USA},

232 doi = {http://doi.{ACM}.org/10.1145/1863495.1863497},

233 publisher = {{ACM}},

234 address = {New York, NY, USA},

237@inproceedings{padsml,

238 author = {Yitzhak Mandelbaum and

239 Kathleen Fisher and

240 David Walker and

241 Mary F. Fern{\'a}ndez and

242 Artem Gleyzer},

243 title = {{PADS/ML}: a functional data description language},

244 booktitle = {POPL '07: Proceedings of the 34th {ACM} {SIGPLAN}-SIGACT Symposium on

245 Principles of Programming Languages, POPL 2007, Nice, France,

246 January 17-19, 2007},

247 year = {2007},

248 pages = {77-83},

249 ee = {http://doi.{ACM}.org/10.1145/1190216.1190231},

250 crossref = {DBLP:conf/popl/2007},

251 bibsource = {DBLP, http://dblp.uni-trier.de}

254@proceedings{DBLP:conf/popl/2007,

255 editor = {Martin Hofmann and

256 Matthias Felleisen},

257 title = {Proceedings of the 34th {ACM} {SIGPLAN}-SIGACT Symposium on

258 Principles of Programming Languages, POPL 2007, Nice, France,

259 January 17-19, 2007},

260 booktitle = {POPL},

261 publisher = {{ACM}},

262 year = {2007},

263 isbn = {1-59593-575-4},

264 bibsource = {DBLP, http://dblp.uni-trier.de}

267@inproceedings{melange,

268 author = {Madhavapeddy, Anil and Ho, Alex and Deegan, Tim and Scott, David and Sohan, Ripduman},

269 title = {Melange: creating a "functional" internet},

270 booktitle = {EuroSys '07: Proceedings of the 2nd {ACM} SIGOPS/EuroSys European Conference on Computer Systems 2007},

271 year = {2007},

272 isbn = {978-1-59593-636-3},

273 location = {Lisbon, Portugal},

274 doi = {http://doi.{ACM}.org/10.1145/1272996.1273009},

275 publisher = {{ACM}},

276 address = {New York, NY, USA},

281@article{next700data,

282 author = {Fisher, Kathleen and Mandelbaum, Yitzhak and Walker, David},

283 title = {The next 700 data description languages},

284 journal = {{SIGPLAN} Not.},

285 volume = {41},

286 number = {1},

287 year = {2006},

288 issn = {0362-1340},

289 pages = {2--15},

290 doi = {http://doi.{ACM}.org/10.1145/1111320.1111039},

291 publisher = {{ACM}},

292 address = {New York, NY, USA},

296@INPROCEEDINGS{xi-ats,

297 author = {Hongwei Xi},

298 title = {{Applied Type System} (extended abstract)},

299 booktitle = {Types for Proofs and Programs 2003},

300 editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},

301 publisher = {Springer},

302 series = {Lecture Notes in Computer Science},

303 volume = {3085},

304 year = {2004},

305 pages = {394--408}

308@inproceedings{powerpi,

309 author = {Nicolas Oury and

310 Wouter Swierstra},

311 title = {The power of {Pi}},

312 booktitle = {{ICFP} '08: Proceedings of the 13th {ACM} {SIGPLAN} International Conference

313 on Functional Programming, {ICFP} 2008, Victoria, BC, Canada,

314 September 20-28, 2008},

315 year = {2008},

316 pages = {39--50},

317 ee = {http://doi.{ACM}.org/10.1145/1411204.1411213},

318 crossref = {DBLP:conf/{ICFP}/2008},

319 bibsource = {DBLP, http://dblp.uni-trier.de}

322@proceedings{DBLP:conf/{ICFP}/2008,

323 editor = {James Hook and

324 Peter Thiemann},

325 title = {Proceeding of the 13th {ACM} {SIGPLAN} international conference

326 on Functional programming, {ICFP} 2008, Victoria, BC, Canada,

327 September 20-28, 2008},

328 booktitle = {{ICFP}},

329 publisher = {{ACM}},

330 year = {2008},

331 isbn = {978-1-59593-919-7},

332 bibsource = {DBLP, http://dblp.uni-trier.de}

336@inproceedings{security-types,

337 author = {Morgenstern, Jamie and Licata, Daniel R.},

338 title = {Security-typed programming within dependently typed programming},

339 booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},

340 year = {2010},

341 isbn = {978-1-60558-794-3},

342 pages = {169--180},

343 location = {Baltimore, Maryland, USA},

344 doi = {http://doi.{ACM}.org/10.1145/1863543.1863569},

345 publisher = {{ACM}},

346 address = {New York, NY, USA},

349@inproceedings{levitation,

350 author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},

351 title = {The gentle art of levitation},

352 booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},

353 year = {2010},

354 isbn = {978-1-60558-794-3},

355 pages = {3--14},

356 location = {Baltimore, Maryland, USA},

357 doi = {http://doi.{ACM}.org/10.1145/1863543.1863547},

358 publisher = {{ACM}},

359 address = {New York, NY, USA},

364@INPROCEEDINGS{awkward,

365 author = {Simon {Peyton Jones}},

366 title = {Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in {Haskell}},

367 booktitle = {Engineering theories of software construction},

368 year = {2001},

369 pages = {47--96}

372@inproceedings{scrap-engine,

373 author = {Brady, Edwin and Hammond, Kevin},

374 title = {Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation},

375 booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},

376 year = {2010},

377 isbn = {978-1-60558-794-3},

378 pages = {297--308},

379 location = {Baltimore, Maryland, USA},

380 doi = {http://doi.{ACM}.org/10.1145/1863543.1863587},

381 publisher = {{ACM}},

382 address = {New York, NY, USA},

385@article{urweb,

386 author = {Chlipala, Adam},

387 title = {Ur: statically-typed metaprogramming with type-level record computation},

388 journal = {{SIGPLAN} Not.},

389 volume = {45},

390 number = {6},

391 year = {2010},

392 issn = {0362-1340},

393 pages = {122--133},

394 doi = {http://doi.{ACM}.org/10.1145/1809028.1806612},

395 publisher = {{ACM}},

396 address = {New York, NY, USA},

401@phdthesis{norell-thesis,

402 author = {Ulf Norell},

403 title = {Towards a practical programming language based on dependent type

404 theory},

405 school = {Chalmers University of Technology},

406 year = 2007,

407 month = {September},

410@inproceedings{open-type,

411 author = {Schrijvers, Tom and Peyton Jones, Simon and Chakravarty, Manuel and Sulzmann, Martin},

412 title = {Type checking with open type functions},

413 booktitle = {International Conf. on Functional Programming ({ICFP} 2008)},

414 year = {2008},

415 pages = {51--62},

416 doi = {http://doi.{ACM}.org/10.1145/1411203.1411215},

417 publisher = {{ACM}},

418 address = {New York, NY, USA},

421@inproceedings{ngna-dsl,

422 title = {Domain Specific Languages ({DSL}s) for Network Protocols},

423 author = {Saleem Bhatti and Edwin Brady and Kevin Hammond and James McKinna},

424 year = {2009},

425 booktitle = {International Workshop on Next Generation Network Architecture ({NGNA} 2009)}

428@phdthesis{gill-thesis,

429 title = {Cheap deforestation for non-strict functional languages},

430 author = {A Gill},

431 institution = {University of Glasgow},

432 month = {January},

433 year = 1996

436@misc{llvm-haskell,

437 title = {Low Level Virtual Machine for {Glasgow Haskell Compiler}},

438 author = {David Terei},

439 year = 2009,

440 howpublished = {Bachelor's Thesis, Computer Science and Engineering Dept., The University of New South Wales, Sydney, Australia}

443@mastersthesis{llvm,

444 title = {{LLVM}: An Infrastructure for Multi-Stage Optimization},

445 author = {Chris Lattner},

446 year = 2002,

447 month = {December},

448 institution = {Computer Science Dept., University of Illinois at Urbana-Champaign}

451@inproceedings{gpu-arrays,

452 title = {GPU Kernels as Data-Parallel Array Computations in Haskell},

453 author = {Sean Lee and Manuel M. T. Chakravarty and Vinod Grover and Gabriele Keller.},

454 year = 2009,

455 booktitle = {Workshop on Exploiting Parallelism using GPUs and other Hardware-Assisted Methods (EPAHM 2009)}

458@misc{cryptol,

459 author = {Galois, Inc.},

460 title = {Cryptol},

461 year = {2009},

462 howpublished = {\url{http://cryptol.net/}}

465@inproceedings{paradise-dsl,

466 author = {Lennart Augustsson and Howard Mansell and Ganesh Sittampalam},

467 title = {{Paradise: a two-stage DSL embedded in Haskell}},

468 booktitle = {International Conf. on Functional Programming ({ICFP} 2008)},

469 year = {2008},

470 publisher = {{ACM}},

471 pages = {225--228}

474@misc{dsl-bib,

475 author = {Arie {van Deursen} and Paul Klint and Joost Visser},

476 title = {Domain-Specific Languages --- an annotated bibliography},

477 year = 2000,

478 howpublished = {\url{http://homepages.cwi.nl/~arie/papers/dslbib/}}

481@inproceedings{imperative-pe,

482 author = {Debois, S{\o}ren},

483 title = {Imperative program optimization by partial evaluation},

484 booktitle = {PEPM '04: Proceedings of the 2004 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},

485 year = {2004},

486 isbn = {1-58113-835-0},

487 pages = {113--122},

488 location = {Verona, Italy},

489 doi = {http://doi.{ACM}.org/10.1145/1014007.1014019},

490 publisher = {{ACM}},

491 address = {New York, NY, USA},

495@inproceedings{offline-pe-termination,

496 author = {Andersen, Peter Holst and Holst, Carsten Kehler},

497 title = {Termination Analysis for Offline Partial Evaluation of a Higher Order Functional Language},

498 booktitle = {Proc. SAS '96: Intl. Symp. on Static Analysis},

499 year = {1996},

500 isbn = {3-540-61739-6},

501 pages = {67--82},

502 publisher = {Springer},

503 notaddress = {London, UK},

507@inproceedings{stage-duplication,

508 author = {Swadi, Kedar and Taha, Walid and Kiselyov, Oleg and Pasalic, Emir},

509 title = {A monadic approach for avoiding code duplication when staging memoized functions},

510 notbooktitle = {PEPM '06: Proceedings of the 2006 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},

511 booktitle = {Proc. PEPM '06:{ACM} Symp. on Partial Evaluation and Semantics-based Program Manipulation},

512 year = {2006},

513 isbn = {1-59593-196-1},

514 pages = {160--169},

515 location = {Charleston, South Carolina},

516 doi = {http://doi.{ACM}.org/10.1145/1111542.1111570},

517 notpublisher = {{ACM}},

518 notaddress = {New York, NY, USA},

522@inproceedings{concoqtion,

523 author = {Fogarty, Seth and Pasalic, Emir and Siek, Jeremy and Taha, Walid},

524 title = {Concoqtion: indexed types now!},

525 booktitle = {PEPM '07: Proceedings of the 2007 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},

526 year = {2007},

527 isbn = {978-1-59593-620-2},

528 pages = {112--121},

529 location = {Nice, France},

530 doi = {http://doi.{ACM}.org/10.1145/1244381.1244400},

531 publisher = {{ACM}},

532 address = {New York, NY, USA},

535@inproceedings{metahaskell,

536 author = "Tim Sheard and Simon {Peyton Jones}",

537 title = "Template metaprogramming for {Haskell}",

538 booktitle = "{ACM} Haskell Workshop",

539 year = 2002,

540 month = oct,

541 pages = "1-16",

542 noteditor = "Manuel M. T. Chakravarty",

543 notpublisher = "{ACM} Press"

546@misc{shark-profiler,

547 title = {Optimizing your application with {Shark 4}},

548 year = 2009,

549 howpublished = {\url{http://developer.apple.com/tools/sharkoptimize.html}}

552@misc{shootout,

553 title = {The Computer Language Benchmark Game},

554 year = {2009},

555 howpublished = {\url{http://shootout.alioth.debian.org/}}

558@article{futamura,

559 author = {Yoshihiko Futamura},

560 year = 1971,

561 title = "Partial Evaluation of Computation Process --– An Approach to a Compiler-Compiler",

562 journal = {Systems, Comps., Controls},

563 volume = 2,

564 number = 5,

565 pages = {45-–50}

568@book{pebook,

569 title = {Partial Evaluation and Automatic Program Generation},

570 author = {N.D. Jones and C.K. Gomard and P. Sestoft},

571 year = 1993,

572 publisher = {Prentice Hall International}

575@inproceedings{pantheon,

576 author = {Sean Seefried and Manuel Chakravarty and Gabriele Keller},

577 title = {Optimising Embedded {DSLs} using {Template Haskell}},

578 year = {2004},

579 booktitle = {{Proc. GPCE~'04: Conf. Generative Prog. and Component Eng.}},

580 publisher = {Springer},

581 series = {LNCS}

584@article{pan,

585 author = {Elliott, Conal and Finne, Sigbj\orn and De Moor, Oege},

586 title = {Compiling embedded languages},

587 journal = {J. Funct. Program.},

588 volume = {13},

589 number = {3},

590 year = {2003},

591 issn = {0956-7968},

592 pages = {455--481},

593 doi = {http://dx.doi.org/10.1017/S0956796802004574},

594 publisher = {Cambridge University Press},

595 address = {New York, NY, USA},

599@inproceedings{russell,

600 author = {Sozeau, Matthieu},

601 title = {Program-ing finger trees in Coq},

602 booktitle = {{ICFP} '07: Proceedings of the 12th {ACM} {SIGPLAN} international conference on Functional programming},

603 year = {2007},

604 isbn = {978-1-59593-815-2},

605 pages = {13--24},

606 location = {Freiburg, Germany},

607 doi = {http://doi.{ACM}.org/10.1145/1291151.1291156},

608 publisher = {{ACM}},

609 address = {New York, NY, USA},

612@inproceedings{turner-total,

613 author = {D. A. Turner},

614 title = {Elementary Strong Functional Programming},

615 year = 1995,

616 booktitle = "First International Symposium on Functional Programming Languages in Education",

617 publisher = {Springer},

618 series = {LNCS},

619 volume = {1022},

620 pages = {1--13}

623@incollection{free-theorems,

624 author = "P. Wadler",

625 title = "Theorems for Free!",

626 booktitle = "{Proc. 4th Int.\ Conf.\ on Funct.\ Prog.\ Languages and Computer Arch., {FPCA}'89, London, {UK}, 11--13 Sept 1989}",

627 publisher = "{ACM} Press",

628 address = "New York",

629 pages = "347--359",

630 year = "1989",

631 url = "citeseer.ist.psu.edu/wadler89theorems.html"

634@inproceedings{TrulyConcurrent,

635 author = {Naiyong Jin and Jifeng He},

636 title = {Towards A Truly Concurrent Model for Processes Sharing Resources},

637 booktitle = {Proc. 3rd {IEEE} International Conf. on Soft. Eng. and Formal Methods},

638 year = {2005},

639 isbn = {0-7695-2435-4},

640 pages = {231--239},

641 doi = {http://dx.doi.org/10.1109/SEFM.2005.50},

642 publisher = {{IEEE} Computer Society},

643 address = {Washington, DC, USA},

646@misc{GPCE2006,

647 note = {Omitted to preserve anonymity, contact PC chair for details}

650@misc{IFL2006,

651 note = {Omitted to preserve anonymity, contact PC chair for details}

654@misc{ivor-anon,

655 note = {Omitted to preserve anonymity, contact PC chair for details}

658@inproceedings{HaskellIO,

659 author = {Simon L. {Peyton Jones} and Philip Wadler},

660 title = {Imperative functional programming},

661 booktitle = {Proc. 20th {ACM} Symposium on Principles of programming languages},

662 year = {1993},

663 isbn = {0-89791-560-7},

664 pages = {71--84},

665 location = {Charleston, South Carolina, United States},

666 doi = {http://doi.{ACM}.org/10.1145/158511.158524},

667 publisher = {{ACM}},

668 address = {New York, NY, USA},

671@article{CorrectnessConstruction,

672author = "P. Amey",

673title = "{Correctness by Construction: Better can also be Cheaper}",

674journal = "{CrossTalk: the Journal of Defense Software Engineering}",

675month = mar,

676year = 2002,

677pages = "24--28"

682@INPROCEEDINGS{hj:popl03,

683 AUTHOR = {M. Hofmann and S. Jost},

684 TITLE = {Static Prediction of Heap Space Usage for First-Order Function

685al Programs},

686booktitle = "Proc. {POPL 2003 --- 2003 {ACM} Symp. on Principles of Programming La

687nguages}",

688 KEY = {HJ_POPL03},

689 PAGES = {185--197},

690 YEAR = {2003},

691 ORGANIZATION = {{ACM}}

695@article{kobayashi-lock,

696 author = {Naoki Kobayashi},

697 title = {A type system for lock-free processes},

698 journal = {Inf. Comput.},

699 volume = {177},

700 number = {2},

701 year = {2002},

702 issn = {0890-5401},

703 pages = {122--159},

704 doi = {http://dx.doi.org/10.1016/S0890-5401(02)93171-8},

705 publisher = {Academic Press, Inc.},

706 address = {Duluth, MN, USA},

709@techreport{linear-alias,

710 title = {Linear types for aliased resources},

711 author = {Chris Hawblitzel},

712 year = {2005},

713 institution = {Microsoft Research},

714 number = {MSR-TR-2005-141}

717@article{kobayashi-esop,

718 title = {Type-Based Analysis of Deadlock fora Concurrent Calculus with Interrupts},

719 author = {Kohei Suenaga and Naoki Kobayashi},

720 year = {2007},

721 booktitle = {ESOP}

724@inproceedings{res-c,

725 title = {A Path Sensitive Type System for Resource Usage Verification of C Like Languages},

726 author = {Hyun-Goo Kang and Youil Kim and Taisook Han and Hwansoo Han},

727 year = 2005,

728 publisher = {Springer-Verlag},

729 booktitle = {Programming Languages and Systems},

730 pages = {264--280},

731 series = {LNCS},

732 volume = {3780}

735@miscs{lsr,

736 title = {Lightweight static resources: Sexy types for embedded and systems programming},

737 author = {Oleg Kiselyov and Chung-Chieh Shan},

738 year = 2007,

739 note = {Draft}

742@inproceedings{scoped-res,

743 title = {Resource Usage Analysis Via Scoped Methods},

744 author = {Gang Tan and Xinming Ou and David Walker},

745 booktitle = {Foundations of Object-Oriented Languages},

746 year = {2003}

749@article{igarashi-res,

750 author = {Igarashi, Atsushi and Kobayashi, Naoki},

751 title = {Resource usage analysis},

752 journal = {ACM Trans. Program. Lang. Syst.},

753 volume = {27},

754 issue = {2},

755 month = {March},

756 year = {2005},

757 issn = {0164-0925},

758 pages = {264--313},

759 numpages = {50},

760 url = {http://doi.acm.org/10.1145/1057387.1057390},

761 doi = {http://doi.acm.org/10.1145/1057387.1057390},

762 acmid = {1057390},

763 publisher = {ACM},

764 address = {New York, NY, USA},

765 keywords = {Resource usage, type inference},

768@phdthesis{monitoring,

769 title = {Policy Enforcement via Program Monitoring},

770 author = {Jarred Adam Ligatti},

771 year = 2006,

772 month = {May}

775@inproceedings{sec-policy,

776 title = {A Type System for Expressive Security Policies},

777 author = {David Walker},

778 booktitle = {Twenty-Seventh {ACM} {SIGPLAN} Symposium on Principles of Programming Languages},

779 pages = {254--267},

780 year = 2000}

782@inproceedings{res-dfa,

783 author = {K. Marriott and P.J. Stuckey and M. Sulzmann},

784 title = {Resource Usage Verification},

785 year = 2003,

786 booktitle = {In Proc. of First Asian Symposium, APLAS 2003},

787 pages = {212--229},

788 publisher = {Springer-Verlag}

791@incollection{ hancock-interactive,

792 author = "Peter Hancock and Anton Setzer",

793 title = "Interactive Programs in Dependent Type Theory",

794 booktitle = "Proc.\ of 14th Ann.\ Conf.\ of {EACSL}, {CSL}'00, Fischbau, Germany, 21--26 Aug 2000",

795 volume = "1862",

796 publisher = "Springer-Verlag",

797 address = "Berlin",

798 editor = "P. Clote and H. Schwichtenberg",

799 pages = "317--331",

800 year = "2000",

801 url = "citeseer.ist.psu.edu/hancock00interactive.html" }

803@inproceedings{popeea-resources,

804 author = {Corneliu Popeea and Wei-Ngan Chin},

805 title = {A type system for resource protocol verification and its correctness proof},

806 booktitle = {PEPM '04: Proceedings of the 2004 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},

807 year = {2004},

808 isbn = {1-58113-835-0},

809 pages = {135--146},

810 location = {Verona, Italy},

811 doi = {http://doi.{ACM}.org/10.1145/1014007.1014021},

812 publisher = {{ACM} Press},

813 address = {New York, NY, USA},

816@inproceedings{sheard-langfuture,

817 author = {Tim Sheard},

818 title = "Languages of the future",

819 booktitle = "{ACM} Conference on Object Orientated Programming Systems, Languages and Applicatioons (OOPSLA'04)",

820 year = "2004"

823@inproceedings{ivor,

824 author = {Edwin Brady},

825 title = {{Ivor}, a proof engine},

826 year = {2007},

827 publisher = {Springer-Verlag},

828 series = {LNCS},

829 booktitle = {Implementation and Application of Functional Languages 2006}

832@misc{coq-in-coq,

833 author = {Bruno Barras and Benjamin Werner},

834 year = 1997,

835 title = {{Coq} in {Coq}}

838@article{hudak-edsl,

839 author = {Paul Hudak},

840 title = {Building Domain-Specific Embedded Languages},

841 year = {1996},

842 month = {December},

843 journal = {{ACM} Computing Surveys},

844 volume = {28A},

845 number = {4}

848@inproceedings{concon,

849 author = {Conor McBride and Healfdene Goguen and James McKinna},

850 title = {Some Constructions On Constructors},

851 year = 2005,

852 booktitle = {TYPES 2004},

853 publisher = {Springer},

854 series = {LNCS},

855 volume = {3839}

858@InProceedings{Hume-GPCE,

859author = {K. Hammond and G.J. Michaelson},

860title = {{Hume: a Domain-Specific Language for Real-Time Embedded Systems}},

861booktitle = {{Proc. Conf. Generative Programming and Component Engineering (GPCE~'03)}},

862publisher = {Springer-Verlag},

863series = {Lecture Notes in Computer Science},

864year = {2003},

867@inproceedings{lcf-milner,

868 author = {Robin Milner},

869 title = {{LCF}: A Way of Doing Proofs with a Machine},

870 booktitle = {Mathematical Foundations of Computer Science 1978},

871 pages = {146-159},

872 year = 1979,

873 series = {LNCS},

874 volume = {64}

878@inproceedings{epireloaded,

879 title = {Epigram Reloaded: A Standalone Typechecker for {ETT}},

880 author = {James Chapman and Thorsten Altenkirch and Conor McBride},

881 year = 2006,

882 booktitle = {Trends in Functional Programming 2005},

883 note = {To appear}

886@TECHREPORT{why-tool,

887 AUTHOR = {J.-C. Filli\^atre},

888 TITLE = {{Why: a multi-language multi-prover verification tool}},

889 INSTITUTION = {{LRI, Universit\'e Paris Sud}},

890 TYPE = {{Research Report}},

891 NUMBER = {1366},

892 MONTH = {March},

893 YEAR = 2003,

894 URL = {http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz}

897@misc{ large-extraction,

898 author = "Lu\'iz Cruz-Filipe and Bas Spitters",

899 title = "Program Extraction from Large Proof Developments",

900 year = 2003,

901 url = "citeseer.ist.psu.edu/cruz-filipe03program.html" }

903@inproceedings{ fta,

904 author = "Herman Geuvers and Freek Wiedijk and Jan Zwanenburg",

905 title = "A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals",

906 booktitle = "{TYPES 2000}",

907 pages = "96--111",

908 year = "2000",

909 url = "citeseer.ist.psu.edu/geuvers01constructive.html" }

911@article{mckinna-expr,

912 title = {A type-correct, stack-safe, provably correct, expression compiler in {Epigram}},

913 author = {James McKinna and Joel Wright},

914 year = 2007,

915 journal = {Journal of Functional Programming},

916 note = {To appear}

919@article{pugh-omega,

920 title = "The {Omega} {Test}: a fast and practical integer programming algorithm for dependence analysis",

921 author = "William Pugh",

922 journal = "Communication of the {ACM}",

923 year = 1992,

924 pages = {102--114}

927@misc{four-colour,

928 author = "Georges Gonthier",

929 title = "A computer-checked proof of the {Four Colour Theorem}",

930 year = 2005,

931 howpublished = {\url{http://research.microsoft.com/~gonthier/4colproof.pdf}}}

933@inproceedings{sparkle,

934 author = "Maarten {de Mol} and Marko {van Eekelen} and Rinus Plasmeijer",

935 title = "Theorem Proving for Functional Programmers",

936 url = "citeseer.ist.psu.edu/654423.html",

937 BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2002)},

938 publisher = {Springer},

939 series = {LNCS},

940 volume = {2312},

941 year = 2002

944@misc{agda,

945 title = {Agda},

946 author = {Catarina Coquand},

947 howpublished= {\url{http://agda.sourceforge.net/}},

948 year = 2005

951@misc{cover,

952 title = {Cover Translator},

953 howpublished = {\url{http://coverproject.org/CoverTranslator/}}

956@misc{parsec,

957 title = {Parsec, a fast combinator parser},

958 author = {Daan Leijen},

959 year = {2001},

960 howpublished = {\url{http://www.cs.uu.nl/~daan/parsec.html}}

963@inproceedings{dtpmsp-gpce,

964 author = {Edwin Brady and Kevin Hammond},

965 title = {A Verified Staged Interpreter is a Verified Compiler},

966 booktitle = {{Proc. Conf. Generative Programming and Component Engineering (GPCE~'06)}},

967 year = 2006

970@misc{haddock,

971 title = {Haddock: A {Haskell} Documentation Tool},

972 howpublished = {\url{http://www.haskell.org/haddock/}}

975@inproceedings{offshoring,

976 title = {Implicitly Heterogeneous Multi-Stage Programming},

977 author = {Jason Eckhardt and Roumen Kaibachev and Emir Pa\v{s}al\'{i}c and Kedar Swadi and Walid Taha},

978 booktitle = {Proc. 2005 Conf. on Generative Programming and Component Engineering (GPCE 2005)},

979 publisher = {Springer},

980 series = {LNCS},

981 volume = {3676},

982 year = 2005

985@misc{alti-partial,

986 title = {Stop thinking about bottoms when writing programs},

987 author = {Thorsten Altenkirch},

988 year = 2006,

989 note = {Talk at BCTCS 2006}

992@misc{tarmo-partial,

993 title = {Partiality is an Effect},

994 author = {Tarmo Uustalu},

995 year = 2004,

996 note = {Talk at Dagstuhl workshop on Dependently Typed Progamming}

999@inproceedings{McKinnaPOPL06,

1000 author = {James McKinna},

1001 title = {Why dependent types matter},

1002 booktitle = {Proc. {ACM} Symp. on Principles of Programming Languages (POPL 2006)},

1003 year = {2006},

1004 issn = {0362-1340},

1005 pages = {1--1},

1006 doi = {http://doi.{ACM}.org/10.1145/1111320.1111038},

1010@inproceedings{leroy-compiler,

1011 title = {Formal Certification of a Compiler Back-end},

1012 author = {Xavier Leroy},

1013 year = 2006,

1014 booktitle = {Principles of Programming Languages 2006},

1015 pages = {42--54},

1016 publisher = {{ACM} Press}

1019@inproceedings{hutton-exceptions,

1020 title = {Compiling Exceptions Correctly},

1021 year = 2004,

1022 author = {Graham Hutton and Joel Wright},

1023 booktitle = {Mathematics of Program Construction},

1024 publisher = {Springer},

1025 series = {LNCS},

1026 volume = {3125}

1029@inproceedings{tagless-staged,

1030 title = {Tagless Staged Interpreters for Typed Languages},

1031 year = {2002},

1032 booktitle = {Proc. 2002 International Conf. on Functional Programming ({ICFP} 2002)},

1033 author = {Emir Pa\v{s}al\'{i}c and Walid Taha and Tim Sheard},

1034 publisher = {{ACM}}

1037@inproceedings{env-classifiers,

1038 title = {Environment Classifiers},

1039 year = 2003,

1040 author = {Walid Taha},

1041 booktitle = {Proc. {ACM} Symp. on Principles of Programming Languages (POPL 2003)},

1042 pages = {26--37},

1045@inproceedings{dsl-msp,

1046 title = {{DSL} Implementation in {MetaOCaml}, {Template Haskell}, {and C++}},

1047 booktitle = {Domain Specific Program Genearation 2004},

1048 author = {Krzysztof Czarnecki and John O'Donnell and J\"{o}rg Striegnitz and Walid Taha},

1049 publisher = {Springer},

1050 series = {LNCS},

1051 volume = {3016},

1052 year = 2004

1055@misc{ gadt-extk,

1056 author = {Tim Sheard and James Hook and Nathan Linger},

1057 title = {{GADTs} + Extensible Kinds = Dependent Programming},

1058 year = 2005,

1059 misc = {Submitted to {ICFP} '05}

1062@INPROCEEDINGS{dt-framework,

1063 TITLE = {A Dependently Typed Framework for Static Analysis of Program Execution Costs},

1064 YEAR = {2006},

1065 BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2005)},

1066 AUTHOR = {Edwin Brady and Kevin Hammond},

1067 VOLUME = {4015},

1068 SERIES = {LNCS},

1069 PAGES = {74--90},

1070 PUBLISHER = {Springer}

1073@INPROCEEDINGS{step-counting,

1074 TITLE = {Accurate Step Counting},

1075 YEAR = {2006},

1076 BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2005)},

1077 AUTHOR = {Catherine Hope and Graham Hutton},

1078 PUBLISHER = {Springer}

1081@misc{multi-taha,

1082 author = {Walid Taha},

1083 title = {{A Gentle Introduction to Multi-stage Programming}},

1084 year = {2003},

1085 note = {Available from \url{http://www.cs.rice.edu/~taha}},

1086 notnote = {Available from \url{http://www.cs.rice.edu/~taha/publications/journal/dspg04a.pdf}}

1089@misc{mckinnabrady-phase,

1090 title = {Phase Distinctions in the Compilation of {Epigram}},

1091 year = 2005,

1092 author = {James McKinna and Edwin Brady},

1093 note = {Draft}

1096@phdthesis{ brady-thesis,

1097 author = {Edwin Brady},

1098 title = {Practical Implementation of a Dependently Typed Functional Programming Language},

1099 year = 2005,

1100 school = {University of Durham}

1103@phdthesis{ taha-thesis,

1104 author = {Walid Taha},

1105 title = {Multi-stage Programming: Its Theory and Applications},

1106 year = 1999,

1107 school = {Oregon Graduate Inst. of Science and Technology}

1110@phdthesis{ pasalic-thesis,

1111 author = {Emir Pa\v{s}al\'{i}c},

1112 title = {The Role of Type-Equality in Meta-programming},

1113 year = 2004,

1114 school = {OGI School of Science and Engineering}

1117@misc{ydtm,

1118 author = {Thorsten Altenkirch and Conor McBride and James McKinna},

1119 title = {Why Dependent Types Matter},

1120 note = {Draft},

1121 year = 2005}

1124@inproceedings { wadler-listless,

1125 author = {Philip Wadler},

1126 title = {Listlessness is better than laziness: {Lazy} evaluation and garbage collection at compile-time},

1127 booktitle = {Proceedings of the 1984 {ACM} Symposium on LISP and functional programming},

1128 year = 1984,

1129 pages = {45--52}

1132@techreport { gofer-impl,

1133 author = {Mark P. Jones},

1134 title = {The implementation of the Gofer functional programming system},

1135 month = {May},

1136 year = {1994},

1137 number = {YALEU/DCS/RR-1030},

1138 institution = {Yale University}

1141@techreport { pm-opt1,

1142 author = {Kevin Scott and Norman Ramsey},

1143 title = {When do match-compilation heuristics matter?},

1144 month = {May},

1145 year = {2000},

1146 number = {CS-2000-13},

1147 institution = {Department of Computer Science, University of Virginia}

1150@inproceedings{ pm-opt2,

1151 author = "Fabrice Le Fessant and Luc Maranget",

1152 title = "Optimizing Pattern Matching",

1153 booktitle = "International Conference on Functional Programming",

1154 pages = "26-37",

1155 year = "2001",

1156 url = "citeseer.ist.psu.edu/lefessant01optimizing.html" }

1158@incollection{con-engine,

1159 author = {G\'{e}rard Huet},

1160 title = {The constructive engine},

1161 booktitle = {A Perspective in Theoreticak Computer Science},

1162 publisher = {World Scientific Publishing},

1163 year = {1989},

1164 editor = {R. Narasimhan},

1165 note = {Commemorative Volume for Gift Siromoney},

1166 pages = {38--69}

1169@inproceedings{gadts,

1170 title = {Simple unification-based type inference for {GADTs}},

1171 author = {Simon {Peyton Jones} and Dimitrios Vytiniotis and Stephanie Weirich and Geoffrey Washburn},

1172 year = {2006},

1173 booktitle = {Proc. 2006 International Conf. on Functional Programming ({ICFP} 2006)}

1176@misc{wobbly,

1177 author = {Simon {Peyton Jones} and Geoffrey Washburn and Stephanie Weirich},

1178 title = {Wobbly types: type inference for generalised algebraic data types},

1179 year = {2004},

1180 note = {Submitted to POPL 2005}

1183@misc{epigram-afp,

1184 author = {Conor McBride},

1185 title = {Epigram: Practical Programming with Dependent Types},

1186 year = {2004},

1187 howpublished = {Lecture Notes, International Summer School on Advanced Functional Programming}

1190@book{ml85,

1191 author = {Per Martin-L\"{o}f},

1192 title = "Intuitionistic Type Theory",

1193 year = "1985",

1194 publisher = "Bibliopolis"

1195}

1197@article{modular-fulllazy,

1198 title = {A Modular Fully Lazy Lambda Lifter in {Haskell}},

1199 author = {Simon {Peyton Jones} and David Lester},

1200 year = {1991},

1201 month = {May},

1202 journal = {Software Practice and Experience},

1203 volume = {21},

1204 number = {5},

1205 pages = {479--506}

1208@article{ghani-jay95,

1209 author = {Barry Jay and Neil Ghani},

1210 title = {The Virtues of Eta-Expansion},

1211 journal = {Journal of Functional Programming},

1212 year = {1995},

1213 volume = {5},

1214 number = {2},

1215 pages = {135-154},

1218@misc{nkpat,

1219 author = {Lennart Augustsson},

1220 title = {n+k patterns},

1221 year = {1993},

1222 howpublished = {Message to the haskell mailing list, Mon, 17 May 93}

1225@article{ danvy98functional,

1226 author = "Olivier Danvy",

1227 title = "Functional Unparsing",

1228 journal = "Journal of Functional Programming",

1229 volume = "8",

1230 number = "6",

1231 pages = "621-625",

1232 year = "1998",

1233 url = "citeseer.ist.psu.edu/danvy98functional.html" }

1235@inproceedings{SeveriPoll94,

1236 author = {Paula Severi and Erik Poll},

1237 booktitle = {Logical Foundations of Computing Science, LFCS'94},

1238 editor = {A. Nerode and Yu. V. Matiyasevich},

1239 number = {813},

1240 pages = {316--328},

1241 publisher = {Springer},

1242 series = {LNCS},

1243 title = {{P}ure {T}ype {S}ystems with {D}efinitions},

1244 year = {1994}

1247@inproceedings{coinductive,

1248 title = {An Application of Co-Inductive Types in Coq: Verification of the Alternating Bit Protocol},

1249 booktitle = {Proceedings of the 1995 Workshop on Types for Proofs and Programs},

1250 series = {LNCS},

1251 year = {1995},

1252 volume = {1158},

1253 pages = {135-152},

1254 publisher = {Springer-Verlag},

1255 author = {Eduardo Gim\'{e}nez}

1258@book{erlang,

1259 author = "Joe Armstrong and Robert Virding and Claes Wikstr{\"o}m and Mike Williams",

1260 title = "Concurrent Programming in Erlang",

1261 edition = "Second",

1262 publisher = "Prentice-Hall",

1263 year = "1996",

1264 url = "citeseer.ist.psu.edu/armstrong93concurrent.html"

1267@PhdThesis{alti:phd93,

1268 author = "Thorsten Altenkirch",

1269 title = "Constructions, Inductive Types and Strong Normalization",

1270 school = "University of Edinburgh",

1271 year = "1993",

1272 month = "November",

1275@inproceedings{coq-modules,

1276 author = "Jacek Chrzaszcz",

1277 title = "Modules in {Coq} Are and Will Be Correct",

1278 year = {2004},

1279 booktitle = {Types for Proofs and Programs 2003},

1280 editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},

1281 publisher = {Springer},

1282 volume = {3085}

1285@inproceedings{comp-polymorphism,

1286 author = "Robert Harper and Greg Morrisett",

1287 title = "Compiling Polymorphism Using Intensional Type Analysis",

1288 year = "1995",

1289 booktitle = "Proceedings of the 22nd {ACM} {SIGPLAN}-SIGACT symposium on Principles of programming languages",

1290 pages = "130 -- 141"

1293@misc{runtime-loader,

1294 author = "Andre Pang",

1295 title = "{GHC} Runtime Loading",

1296 year = "2004",

1297 howpublished = {Available from \verb+http://www.algorithm.com.au/wiki/hacking/haskell.ghc_runtime_loading+}

1300@article{mccarthy-lisp,

1301 author = "John McCarthy",

1302 title = "Recursive Functions of Symbolic Expressions and Their Computation By Machine",

1303 year = "1960",

1304 journal = "Communications of the {ACM}",

1305 volume = "3",

1306 number = "4",

1307 pages = "184--195"

1310@book{stl,

1311 author = " David R. Musser and Atul Saini and Gillmer J. Derge",

1312 title= "The {STL} Tutorial and Reference Guide: {C++} Programming with the Standard Template Library",

1313 year = "2001",

1314 publisher = "Addison Wesley"

1317@misc{ phase-distinction,

1318 author = "Luca Cardelli",

1319 title = "Phase Distinctions in Type Theory",

1320 howpublished = "Manuscript",

1321 year = "1988",

1322 url = "citeseer.ist.psu.edu/cardelli88phase.html" }

1324@book {pierce-types,

1325 author = "Benjamin C. Pierce",

1326 title = "Type and Programming Languages",

1327 year = "2002",

1328 publisher = "MIT Press"

1331@article{ coqcc,

1332 Author = "Thierry Coquand and G\'{e}rard Huet",

1333 title = "The calculus of constructions",

1334 year = "1988",

1335 journal = "Information and Computation",

1336 volume = "76",

1337 pages = "95--120"

1340@article{ miller91jlc,

1341 Author = "Dale Miller",

1342 Title = "A Logic Programming Language with Lambda-Abstraction,

1343 Function Variables, and Simple Unification",

1344 Journal = "Journal of Logic and Computation",

1345 Volume = "1",

1346 Number = "4",

1347 Pages = "497-536",

1348 Year = "1991",

1349 URL = "citeseer.ist.psu.edu/miller91logic.html",

1350 URL = "file://ftp.cis.upenn.edu/pub/papers/miller/jlc91.dvi.Z" }

1352@article{miller-unity,

1353 author = "Dale Miller",

1354 title = "Unification Under a Mixed Prefix",

1355 journal = "Journal of Symbolic Computation",

1356 volume = "14",

1357 pages = "321--358",

1358 year = 1992

1361@inproceedings{ cynthia,

1362 author = "Jon Whittle and Alan Bundy and Richard J. Boulton and Helen Lowe",

1363 title = "An {ML} Editor Based on Proofs-As-Programs",

1364 booktitle = "Automated Software Engineering",

1365 pages = "166-173",

1366 year = "1999",

1367 url = "citeseer.ist.psu.edu/whittle99ml.html" }

1370@misc{ewd340,

1371 title={The Humble Programmer},

1372 author={Edsger Dijkstra},

1373 year={1972},

1374 note={Turing Award Lecture, EWD 340}

1377@misc{fortran,

1378 title={Specifications for the {IBM} Mathematical FORmula TRANslating System, {FORTRAN}},

1379 author={{IBM Applied Science Division}},

1380 key={IBM},

1381 year={1954},

1382 month={November}

1385@inproceedings{quickcheck,

1386 title = {{QuickCheck}: A Lightweight Tool For Random Testing Of {Haskell} Programs},

1387 author = {Koen Claessen and John Hughes},

1388 year = {2000},

1389 booktitle = {International Conference on Functional Programming}

1392@inproceedings{currylam,

1393 title = {Functionality in Combinatory Logic},

1394 author = {Haskell Curry},

1395 year = {1934},

1396 booktitle = {Proc. Nat. Acad. Sci, USA},

1397 volume = {20},

1398 pages = {584--590}

1401@article{churchsimplelam1,

1402 title = {A set of postulates for the foundation of logic},

1403 author = {Alonzo Church},

1404 year = {1932},

1405 journal = {Annals of Mathematics},

1406 volume = {2},

1407 number = {33},

1408 pages = {346--366}

1411@article{churchsimplelam2,

1412 title = {A set of postulates for the foundation of logic},

1413 author = {Alonzo Church},

1414 year = {1933},

1415 journal = {Annals of Mathematics},

1416 volume = {2},

1417 number = {34},

1418 pages = {839--864}

1421@article{churchlam,

1422 title = {A Formulation of the Simple Theory of Types},

1423 author = {Alonzo Church},

1424 year = {1940},

1425 journal = {Journal of Symbolic Logic},

1426 volume = {5},

1427 pages = {56--58}

1430@book{mitchell,

1431 title = {Concepts in Programming Languages},

1432 author = {John C. Mitchell},

1433 year = {2003},

1434 publisher = {Cambridge University Press}

1437@inproceedings{harrison-hol99,

1438 title = {A Machine-Checked Theory of Floating Point Arithmetic},

1439 year = {1999},

1440 booktitle = {Theorem Proving in Higher Order Logics: 12th International Conference, TP},

1441 pages = {113--130},

1442 author = {John Harrison},

1443 crossref = {hol99}

1446@inproceedings{c--,

1447 title = {C--: A portable assembly language},

1448 year = {1997},

1449 booktitle = {Workshop on Implementing Functional Languages, St Andrews},

1450 author = {Simon {Peyton Jones} and Thomas Nordin and Dino Oliva},

1451 crossref = {func-imp97}

1454@proceedings{func-imp97,

1455 title = {Workshop on Implementing Functional Languages, St Andrews},

1456 year = {1997},

1457 editor = {C Clack},

1458 publisher = {Springer-Verlag}

1461@proceedings{hol99,

1462 volume = {1690},

1463 title = {Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs'99},

1464 year = {1999},

1465 editor = {Yves Bertot and Gilles Dowek and Andr{\'e} Hirschowitz and Christine Paul},

1466 publisher = {Springer-Verlag},

1467 address = {Nice, France},

1468 series = {LNCS}

1471@book{mathlogic,

1472 title = {Mathematical Logic and Programming Languages},

1473 year = {1985},

1474 editor = {C.A.R. Hoare and J.C. Shepherdson},

1475 publisher = {Prentice-Hall}

1478@book{automath,

1479 title = {Selected Papers on Automath},

1480 year = {1994},

1481 editor = {S. Abramsky and J. Barwise and K. Fine and H.J. Keisler and A.S. Troelstr},

1482 publisher = {North-Holland}

1485@misc{gimps,

1486 howpublished = {http://www.mersenne.org/prime.htm},

1487 title = {Great Internet Mersenne Prime Search}

1490@misc{haskell-report,

1491 title = {Haskell 98 Language and Libraries --- The Revised Report},

1492 year = {2002},

1493 month = {December},

1494 author = {Simon {Peyton Jones} and others},

1495 howpublished = {Available from \verb+http://www.haskell.org/+}

1498@inproceedings{cayenne-{ICFP},

1499 author = "Lennart Augustsson",

1500 title = "Cayenne - a Language with Dependent Types",

1501 booktitle = "Proc. 1998 International Conf. on Functional Programming ({ICFP} '98)",

1502 pages = "239--250",

1503 year = "1998",

1504 url = "citeseer.nj.nec.com/augustsson98cayenne.html"

1508@misc{equality-cayenne,

1509 howpublished = {\verb+http://www.cs.chalmers.se/~augustss/cayenne/+},

1510 title = {Equality Proofs in Cayenne},

1511 year = {1999},

1512 author = {Lennart Augustsson}

1515@misc{interp-cayenne,

1516 title = {An exercise in dependent types: A well-typed interpreter},

1517 year = {1999},

1518 author = {Lennart Augustsson and Magnus Carlsson}

1521@inproceedings{balaa00fixpoint,

1522 title = {Fix-Point Equations for Well-Founded Recursion in Type Theory},

1523 year = {2000},

1524 booktitle = {Theorem Proving in Higher Order Logics},

1525 pages = {1-16},

1526 author = {Antonia Balaa and Yves Bertot}

1529@inproceedings{isabelle-maple,

1530 title = {Theorems and algorithms: An interface between Isabelle and Maple},

1531 year = {1995},

1532 booktitle = {International Symposium on Symbolic and Algebraic Computation},

1533 author = {Ballarin, C. and Homann, K., and Calmet, J.}

1536@book{barendregt-num,

1537 title = {The Lambda Calculus, Its Syntax and Semantics},

1538 year = {1984},

1539 publisher = {North-Holland},

1540 author = {Henk Barendregt}

1543@book{beiler,

1544 title = {Recreations in the Theory of Numbers},

1545 year = {1964},

1546 publisher = {Dover},

1547 author = {Albert H. Beiler}

1550@article{multidigit,

1551 journal = {Advances in Applied Mathematics},

1552 title = {Multidigit Multiplication for Mathematicians},

1553 year = {1998},

1554 author = {Daniel J. Bernstein}

1557@article{buhler-fox,

1558 journal = {{ACM} Crossroads 2.1.},

1559 month = {September},

1560 title = {The Fox project: A language-structured approach to networking software.},

1561 year = {1995},

1562 author = {Buhler, J.},

1563 note = {Available at http://www.{ACM}.org/crossroads/xrds2-1/foxnet.html}

1566@techreport{burstall91,

1567 title = {Computer Assisted Proof for Mathematics: an Introduction Using the \textsc{Lego} Proof System},

1568 year = {1991},

1569 institution = {University of Edinburgh},

1570 author = {Rod Burstall}

1573@article{plastic,

1574 title = {An Implementation of {LF} with Coercive Subtyping and Universes},

1575 author = {Paul Callaghan and Zhaohui Luo},

1576 journal = {Journal of Automated Reasoning},

1577 volume = {27},

1578 number = {1},

1579 pages = {3--27},

1580 year = {2001}

1583@article{coercive,

1584 title = {Coercive subtyping},

1585 author = {Zhaohui Luo},

1586 journal = {J. Logic Comput.},

1587 volume = {9},

1588 number = {1},

1589 year = {1991},

1590 pages = {105--130}

1593@inproceedings{calmet-homann,

1594 title = {Classification of communication and cooperation mechanisms for logical and symbolic computation systems},

1595 year = {1996},

1596 booktitle = {Proceedings of the First International Workshop 'Frontiers of Combining S},

1597 pages = {133-146},

1598 publisher = {Kluwer},

1599 author = {J. Calmet and K. Homann}

1602@techreport{comm-proofs,

1603 title = {On Communicating Proofs in Interactive Mathematical Documents},

1604 year = {2000},

1605 institution = {Eindhoven University of Technology},

1606 author = {Olga Caprotti and Martijn Oostdijk}

1609@article{prime2999,

1610 title = {How to formally and efficiently prove Prime(2999)},

1611 year = {2001},

1612 author = {Olga Caprotti and Martijn Oostdijk},

1613 journal = {Symbolic Computation and Automated Reasoning},

1614 pages = {114--125}

1617@book{church-num,

1618 title = {The Calculi of Lambda-Conversion},

1619 year = {1941},

1620 publisher = {Princeton University Press},

1621 author = {Alonzo Church}

1624@book{nuprl86,

1625 title = {Implementing Mathematics with the NuPrl Proof Development System},

1626 year = {1986},

1627 publisher = {Prentice-Hall},

1628 address = {NJ},

1629 author = {Constable, Robert L. and others}

1632@book{conway,

1633 title = {On Numbers and Games},

1634 year = {1976},

1635 publisher = {Academic Press},

1636 author = {J.H. Conway}

1639@misc{coq-manual,

1640 howpublished = {\verb+http://coq.inria.fr/+},

1641 title = {The {Coq} Proof Assistant --- Reference Manual},

1642 year = {2009},

1643 author = {{Coq Development Team}}

1646@misc{tt-prog,

1647 month = {June},

1648 title = {Type Theory and Programming},

1649 year = {1994},

1650 author = {Thierry Coquand and Bengt Nordstr\"{o}m and Jan M. Smith and Bj\"{o}rn von Sydow}

1653@book{func-appr,

1654 title = {The Functional Approach to Programming},

1655 year = {1998},

1656 publisher = {Cambridge University Press},

1657 author = {Guy Cousineau and Michel Mauny}

1660@misc{ibmspec,

1661 howpublished = {http://www2.hursley.ibm.com/decimal/},

1662 month = {January},

1663 title = {Standard Decimal Arithmetic Specification},

1664 year = {2001},

1665 author = {Mike Cowlishaw},

1666 note = {\copyright IBM Corporation 2001}

1669@book{dummett,

1670 title = {Elements of Intuitionism},

1671 year = {2000},

1672 edition = {2nd},

1673 publisher = {Oxford: Clarendon},

1674 author = {Michael A.E. Dummet}

1677@article{dybjer94,

1678 title = {Inductive Families},

1679 year = {1994},

1680 author = {Peter Dybjer},

1681 journal = {Formal Aspects Of Computing},

1682 volume = {6},

1683 pages = {440--465}

1686@misc{octave,

1687 howpublished = {http://www.octave.org/},

1688 month = {February},

1689 title = {GNU Octave -- A high-level interactive language for numerical computations},

1690 year = {1997},

1691 author = {John W. Eaton}

1694@book{comp-methods,

1695 title = {Computing methods for scientists and engineers},

1696 year = {1968},

1697 publisher = {Oxford : Clarendon Press},

1698 author = {L. Fox and D.F. Mayers}

1701@misc{guile,

1702 howpublished = {http://www.gnu.org/software/guile/guile.html},

1703 title = {Guile -- Project GNU's extension language},

1704 year = {2001},

1705 author = {{Free Software Foundation}}

1708@article{need-dep,

1709 journal = {Journal of Functional Programming},

1710 number = {4},

1711 volume = {10},

1712 title = {Do we need dependent types?},

1713 year = {2000},

1714 pages = {409-415},

1715 author = {Daniel Fridlender and Mia Indrika}

1718@book{primes-programming,

1719 title = {Primes and Programming -- An Introduction to Number Theory with Computing},

1720 year = {1993},

1721 publisher = {Cambridge University Press},

1722 author = {Peter Giblin}

1725@misc{rec-coq,

1726 month = {May},

1727 title = {A Tutorial on Recursive Types in \textsc{Coq}},

1728 year = {1998},

1729 author = {Eduardo Gim\'{e}nez}

1732@article{goldberg91,

1733 journal = {{ACM} Computing Surveys},

1734 number = {1},

1735 volume = {23},

1736 title = {What every computer scientist should know about floating point arithmetic},

1737 year = {1991},

1738 pages = {5-48},

1739 author = {D. Goldberg}

1742@article{binary-lambda,

1743 journal = {Journal of Functional Programming},

1744 number = {6},

1745 volume = {10},

1746 title = {An adequate and efficient left associated binary numeral system in the $\lambda$-calculus},

1747 year = {2000},

1748 author = {Mayer Goldberg}

1751@book{hol,

1752 title = {Introduction to HOL},

1753 year = {1993},

1754 publisher = {Cambridge University Press},

1755 author = {M. Gordon and T. Melham}

1758@misc{gmp,

1759 howpublished = {Available from \verb+http://www.swox.com/gmp/manual/+},

1760 title = {The {GNU Multiple Precision} Arithmetic Library 4.1.3 --- Manual},

1761 year = {2004},

1762 author = {Torbj\"{o}rn Granlund and others}

1765@article{harrison-fmsd94,

1766 journal = {Formal Methods in System Design},

1767 volume = {5},

1768 title = {Constructing the Real Numbers in {HOL}},

1769 year = {1994},

1770 pages = {35--59},

1771 author = {John Harrison}

1774@book{harrison-thesis,

1775 title = {Theorem Proving with the Real Numbers},

1776 year = {1998},

1777 publisher = {Springer-Verlag},

1778 author = {John Harrison}

1781@techreport{hol-maple,

1782 title = {Reasing about the Reals: the marriage of HOL and Maple},

1783 year = {1993},

1784 institution = {University of Cambridge Computer Laboratory},

1785 author = {John Harrison and Laurent Th\'{e}ry}

1788@misc{coq-tutorial,

1789 howpublished = {http://pauillac.inria.fr/coq},

1790 title = {The \textsc{Coq} Proof Assistant - A Tutorial},

1791 author = {G\'{e}rard Huet and Gilles Kahn and Christine Paulin-Mohring}

1794@misc{restr-haskell,

1795 howpublished = {http://citeseer.nj.nec.com/253599.html},

1796 month = {September},

1797 title = {Restricted Data Types in Haskell},

1798 year = {1999},

1799 author = {John Hughes}

1802@misc{javadec,

1803 howpublished = {http://www2.hursley.ibm.com/decimalj/decimald.html},

1804 month = {September},

1805 title = {Decimal Arithmetic for Java -- a Proposal},

1806 year = {2000},

1807 author = {{IBM Corporation}}

1810@misc{ieee754,

1811 title = {{IEEE} Standard for Binary Floating Point Arithmetic},

1812 year = {1985},

1813 author = {{IEEE Standard 754}}

1816@misc{ieee854,

1817 title = {IEEE Standard for Radix-Independent Floating-Point Arithmetic},

1818 year = {1987},

1819 author = {{IEEE Standard 854}}

1822@inproceedings{jon91,

1823 title = {Completing the Rational and Metric Spaces in \textsc{Lego}},

1824 year = {1991},

1825 booktitle = {Proceedings of the Second Workshop on Logical Frameworks},

1826 author = {Claire Jones}

1829@misc{ typinghaskell,

1830 author = "Mark Jones",

1831 title = "Typing {Haskell} in {Haskell}",

1832 howpublished = "In Haskell Workshop, September 1999.",

1833 year = "1999",

1834 url = "citeseer.ist.psu.edu/article/jones99typing.html" }

1836@article{karatsuba,

1837 journal = {Soviet Physics-Doklady},

1838 volume = {7},

1839 title = {Multiplication of multidigit numbers by automata},

1840 year = {1963},

1841 pages = {595--596},

1842 author = {A. Karatsuba and Y. Ofman}

1845@book{knuth2,

1846 volume = {2},

1847 title = {The Art of Computer Programming - Seminumerical Algorithms},

1848 year = {1969},

1849 publisher = {Addison Wesley},

1850 author = {Donald E. Knuth}

1853@article{next700,

1854 journal = {Communications of the {ACM}},

1855 number = {3},

1856 month = {March},

1857 volume = {9},

1858 title = {The next 700 programming languages},

1859 year = {1966},

1860 author = {P.J. Landin}

1863@techreport{luo-spec,

1864 month = {January},

1865 title = {Program Specification and Data Refinement in Type Theory},

1866 year = {1993},

1867 institution = {Department of Computer Science, University of Edinburgh},

1868 author = {Zhaohui Luo}

1871@phdthesis{luo90,

1872 school = {University of Edinburgh},

1873 title = {An Extended Calculus Of Constructions},

1874 year = {1990},

1875 author = {Zhaohui Luo}

1878@techreport{lego-manual,

1879 title = {\textsc{Lego} Proof Development System: User's Manual},

1880 year = {1992},

1881 institution = {Department of Computer Science, University of Edinburgh},

1882 author = {Zhaohui Luo and Robert Pollack}

1885@inproceedings{alf,

1886 title = {The {ALF} proof editor and its proof engine},

1887 year = {1994},

1888 booktitle = {Formal Proceeding of the 1993 Workshop on Types for Proofs and Programs},

1889 author = {Lena Magnusson and Bengt N\"{o}rdstrom}

1892@misc{happy,

1893 howpublished = {http://www.haskell.org/happy/},

1894 title = {Happy User Guide},

1895 year = {2001},

1896 author = {Simon Marlow and Andy Gill}

1899@inproceedings{generic-haskell,

1900 title = {Generic Haskell, Specifically},

1901 author = {Dave Clarke and Andres L\"{o}h},

1902 editor = {Jeremy Gibbons and Johan Jeuring},

1903 booktitle = {Proceedings of the IFIP TC2 Working Conference on Generic Programming},

1904 year = {2002},

1905 publisher = {Kluwer Academic Publishers},

1906 pages = {21--48}

1909@article{faking-it,

1910 title = {Faking It -- Simulating Dependent Types in {Haskell}},

1911 year = {2002},

1912 author = {Conor McBride},

1913 journal = {Journal of Functional Programming},

1914 volume = {12},

1915 number = {4+5},

1916 pages = {375--392}

1919@misc{mcbride-inverting,

1920 title = {Inverting Inductively Defined Relations in \textsc{Lego}},

1921 year = {1996},

1922 author = {Conor McBride}

1925@phdthesis{mcbride-thesis,

1926 month = {May},

1927 school = {University of Edinburgh},

1928 title = {Dependently Typed Functional Programs and their proofs},

1929 year = {2000},

1930 author = {Conor McBride}

1933@article{mcbride-unification,

1934 title = {First-Order Unification by Structural Recursion},

1935 year = {2003},

1936 author = {Conor McBride},

1937 journal = {Journal of Functional Programming},

1938 volume = {13},

1939 number = {6},

1940 pages = {1061--1075}

1943@misc{mckinna-pollack,

1944 howpublished = {Kluwer Academic Publishers},

1945 title = {Some Lambda Calculus and Type Theory formalized},

1946 year = {1998},

1947 author = {James McKinna and Robert Pollack}

1950@book{num-theory,

1951 title = {An Introduction to the Theory of Numbers},

1952 year = {1980},

1953 publisher = {John Wiley and Sons},

1954 author = {Ivan Niven and Herbert S. Zuckerman}

1957@book{prog-mltt,

1958 title = {Programming in Martin-L\"{o}f's Type Theory -- An Introduction},

1959 year = {1990},

1960 publisher = {Oxford University Press},

1961 author = {Bengt Nordstr\"{o}m and Kent Petersson and Jan M. Smith},

1962 note = {Out of print. Available from http://www.cs.chalmers.se/Cs/Research/Logic}

1965@book{okasaki,

1966 title = {Purely Functional Data Structures},

1967 year = {1998},

1968 publisher = {Cambridge University Press},

1969 author = {Chris Okasaki}

1972@book{arith-systems,

1973 title = {Computer Arithmetic Systems},

1974 year = {1994},

1975 publisher = {Prentice-Hall},

1976 author = {Amos R. Omondi}

1979@book{pj-imp,

1980 title = {The Implementation of Functional Programming Languages},

1981 year = {1987},

1982 publisher = {Prentice-Hall},

1983 author = {Simon {Peyton Jones}}

1986@book{cp-bjc,

1987 title = {Computational Numerical Methods},

1988 year = {1986},

1989 publisher = {John Wiley and Sons},

1990 author = {C. Phillips and B. Cornelius}

1993@book{nag,

1994 title = {The NAG Library: a beginner's guide},

1995 year = {1986},

1996 publisher = {Oxford : Clarendon Press},

1997 author = {Jen Phillips}

2000@misc{believe,

2001 month = {September},

2002 title = {How to Believe a Machine-Checked Proof},

2003 year = {1996},

2004 author = {Robert Pollack}

2007@phdthesis{pollack94,

2008 school = {University of Edinburgh},

2009 title = {The Theory of LEGO -- A Proof Checker for the Extended Calculus of Constructions},

2010 year = {1994},

2011 author = {Robert Pollack}

2014@inproceedings{intel-bug,

2015 series = {LNCS},

2016 volume = {915},

2017 title = {Anatomy of the Pentium Bug},

2018 publisher = {Springer-Verlag},

2019 year = {1995},

2020 pages = {97--107},

2021 author = {V.R. Pratt}

2024@book{maple,

2025 title = {The Maple Handbook: Maple V Release 4},

2026 year = {1996},

2027 publisher = {Springer},

2028 author = {Darren Redfern}

2031@book{crypto,

2032 title = {Applied Cryptography: protocols, algorithms and source code in C.},

2033 year = {1996},

2034 publisher = {Wiley},

2035 author = {Bruce Schneier}

2038@article{adts,

2039 journal = {Mathematical Structures in Computer Science},

2040 number = {2},

2041 volume = {10},

2042 title = {On lists and other abstract data types in the calculus of construction},

2043 year = {2000},

2044 pages = {261-276},

2045 author = {Jonathan P. Seldin}

2048@article{seldin97,

2049 journal = {Annals of Pure and Applied Logic},

2050 number = {1},

2051 month = {January},

2052 volume = {83},

2053 title = {On the proof theory of Coquand's calculus of constructions},

2054 year = {1997},

2055 pages = {23--101},

2056 author = {Jonathan P. Seldin}

2059@article{wichmann,

2060 journal = {The Computer Journal},

2061 volume = {32},

2062 title = {Towards a Formal Specification of Floating Point},

2063 year = {1989},

2064 pages = {432-436},

2065 author = {B.A. Wichmann}

2068@book{mathematica,

2069 title = {Mathematica : a system for doing mathematics by computer},

2070 year = {1991},

2071 publisher = {Addison Wesley},

2072 author = {Stephen Wolfram}

2075@inproceedings{xi-imp,

2076author = "Hongwei Xi",

2077title = {{Imperative Programming with Dependent Types}},

2078booktitle = "Proceedings of 15th {IEEE} Symposium on Logic in Computer Science",

2079year = 2000,

2080month = "June",

2081address = "Santa Barbara",

2082pages = "375--387"

2085@phdthesis{xi-thesis,

2086 month = {December},

2087 school = {Department of Mathematical Sciences, Carnegie Mellon University},

2088 title = {Dependent Types in Practical Programming},

2089 year = {1998},

2090 author = {Hongwei Xi}

2094@techreport{dtal,

2095author = {Hongwei Xi and Robert Harper},

2096title = {A Dependently Typed Assembly Language},

2097institution = {Computer Science and Engineering Department, Oregon Graduate Institute},

2098year = 1999,

2099number = {OGI-CSE-99-008},

2100month = {July},

2103@misc{bignum-cmp,

2104 month = {February},

2105 title = {Comparison of three public-domain multiprecision libraries: BigNum, Gmp and Pari},

2106 year = {1998},

2107 author = {Paul Zimmerman}

2110@book{perl,

2111 title = {Programming Perl},

2112 author = {Larry Wall and Tom Christiansen and Jon Orwant},

2113 year = {2000},

2114 edition = {3rd},

2115 publisher = {O'Reilly}

2118@misc{python,

2119 howpublished = {http://www.python.org/doc/current/tut/tut.html},

2120 month = {April},

2121 title = {Python Tutorial},

2122 year = {2001},

2123 author = {Guido van {Rossum} and Fred L. {Drake, Jr}}

2126@book{logic,

2127 title = {The Language of First Order Logic},

2128 year = {1992},

2129 publisher = {CSLI Lecture Notes},

2130 author = {Jon Barwise and John Etchemendy}

2133@book{haskell,

2134 title = {Haskell -- The Craft of Functional Programming},

2135 year = {1999},

2136 publisher = {Addison Wesley},

2137 author = {Simon Thompson}

2140@inproceedings{coq-hol,

2141 title = {A Comparative Study of Coq and HOL},

2142 year = {1997},

2143 booktitle = {Theorem Proving in Higher Order Logics},

2144 pages = {323-337},

2145 author = {Vincent Zammit}

2148@misc{gay90,

2149 month = {November},

2150 title = {Correctly Rounded Binary-Decimal and Decimal-Binary Conversions},

2151 year = {1990},

2152 author = {David M. Gay},

2153 note = {AT&T Bell Laboratories, Numerical Analysis Manuscript 90-10}

2156@article{hughes-matters,

2157 journal = {Computer Journal},

2158 number = {2},

2159 volume = {32},

2160 title = {Why Functional Programming Matters},

2161 year = {1989},

2162 pages = {98--107},

2163 author = {J. Hughes}

2166@inproceedings{proofpointing,

2167 title = {Proof by Pointing},

2168 year = {1994},

2169 booktitle = {Proceedings of the International Symposium on Theoretical Aspects of Computer So},

2170 pages = {141--160},

2171 editor = {M. Hagiya and J. C. Mitchell},

2172 publisher = {Springer-Verlag},

2173 series = {LNCS},

2174 volume = {789},

2175 address = {Sendai, Japan},

2176 author = {Yves Bertot and Gilles Kahn and Laurent Th{\'e}ry}

2179@misc{inductive-coq,

2180 month = {December},

2181 title = {Inductive Definitions in the System Coq -- Rules and Properties},

2182 year = {1992},

2183 author = {Christine Paulin-Mohring}

2186@misc{leiserson98,

2187 month = {July},

2188 title = {Using de Bruijn Sequences to Index a 1 in a Computer Word},

2189 year = {1998},

2190 author = {{Charles E. Leiserson} and {Harald Prokop} and {Keith H. Randall}}

2193@inproceedings{proofchecking,

2194 title = {A two-level approach towards lean proof-checking},

2195 year = {1996},

2196 booktitle = {TYPES},

2197 pages = {16--35},

2198 author = {G. Barthe and M.P.J. Ruys and H.P. Barendregt}

2201@inproceedings{congruence,

2202 title = {Congruence Types},

2203 year = {1995},

2204 booktitle = {CSL},

2205 pages = {36--51},

2206 author = {Gilles Barthe and Herman Geuvers}

2209@phdthesis{geuvers-thesis,

2210 title = {Logic and Type Systems},

2211 author = {Herman Geuvers},

2212 year = 1993,

2213 school = {Katholieke Universiteit Nijmegen}

2216@techreport{multiple-values,

2217 title = {Multiple Values in {Standard ML}},

2218 year = {1994},

2219 number = {94-312},

2220 institution = {LFCS, Dept of Computer Science, University of Edinburgh},

2221 author = {Kevin Mitchell}

2224@inproceedings{oracle-checking,

2225 month = {January},

2226 title = {Oracle-Based Checking of Untrusted Software},

2227 year = {2001},

2228 booktitle = {Proceedings of the 28th {ACM} Symposium on Principles of Programming Languages},

2229 pages = {142--154},

2230 author = {{George C. Necula} and {S.P. Rahul}}

2233@article{adams93jfp,

2234 journal = {Journal of Functional Programming},

2235 number = {4},

2236 volume = {3},

2237 title = {Efficient Sets -- A Balancing Act},

2238 year = {1993},

2239 pages = {553--561},

2240 author = {Stephen Adams}

2243@inproceedings{hughes-sized,

2244 title = {Proving the Correctness of Reactive Systems Using Sized Types},

2245 year = {1996},

2246 booktitle = {Proceedings of the 23rd {ACM} {SIGPLAN}-SIGACT symposium on Principles of programmin},

2247 pages = {410--423},

2248 author = {John Hughes and Lars Pareto and Amr Sabry}

2251@inproceedings{whittle99ml,

2252 title = {An {ML} Editor Based on Proofs-As-Programs},

2253 year = {1999},

2254 booktitle = {Automated Software Engineering},

2255 pages = {166--173},

2256 author = {Jon Whittle and Alan Bundy and Richard J. Boulton and Helen Lowe}

2259@book{efp-typeinf,

2260 title = {Elements of Functional Programming},

2261 year = {1989},

2262 publisher = {Addison-Wesley},

2263 author = {Chris Reade},

2264 series = {International Computer Science Series}

2267@incollection{ wadler-views,

2268 author = "Philip Wadler",

2269 title = "Views: {A} Way for Pattern Matching to Cohabit with Data Abstraction",

2270 booktitle = "Proceedings, 14th Symposium on Principles of Programming Languages",

2271 publisher = "Association for Computing Machinery",

2272 editor = "Steve Munchnik",

2273 pages = "307--312",

2274 year = "1987",

2275 url = "citeseer.nj.nec.com/wadler87views.html" }

2277@article{ coquand-checking,

2278 author = "Thierry Coquand",

2279 title = "An Algorithm for Type-Checking Dependent Types",

2280 journal = "Science of Computer Programming",

2281 volume = "26",

2282 number = "1-3",

2283 pages = "167-177",

2284 year = "1996",

2285 url = "citeseer.nj.nec.com/coquand96algorithm.html" }

2287@misc{coquand-pm,

2288 author = "Thierry Coquand",

2289 title = "Pattern Matching with Dependent Types",

2290 year = "1992",

2291 howpublished = "Available from \verb+http://www.cs.chalmers.se/~coquand/type.html+"

2294@misc{pollack-records,

2295 month = {August},

2296 title = {Dependently Typed Records for Representing Mathematical Structure},

2297 year = {2000},

2298 author = {Robert Pollack}

2301@article{checking-betarte,

2302 journal = {Journal of Functional Programming},

2303 number = {2},

2304 month = {March},

2305 volume = {10},

2306 title = {Type checking dependent (record) types and subtyping},

2307 year = {2000},

2308 pages = {137--166},

2309 author = {Gustavo Betarte}

2313@article{ gcode,

2314 author = "Thomas Johnsson",

2315 title = "Efficient Compilation of Lazy Evaluation",

2316 booktitle = "Proceedings of the {{ACM}} {{SIGPLAN}}'84 Symposium on Compiler Con struction",

2317 journal = "{SIGPLAN} Notices",

2318 volume = "19",

2319 number = "6",

2320 month = "June",

2321 publisher = "{ACM} Press",

2322 pages = "58--69",

2323 year = "1984",

2324 url = "citeseer.nj.nec.com/johnsson84efficient.html" }

2326@misc{kamareddine01,

2327 month = {February},

2328 title = {Reviewing the classical and the de Bruijn notation for $\lambda$-calculus and pure type systems},

2329 year = {2001},

2330 author = {Fairouz Kamareddine}

2333@book{prooftheory,

2334 title = {Basic Proof Theory},

2335 year = {1996},

2336 publisher = {Cambridge University Press},

2337 author = {A.S. Troelstra and H. Schwichtenberg},

2338 series = {Cambridge Tracts in Theoretical Computer Science}

2341@misc{nbe_staged,

2342 title = {Integrating Normalization-by-Evaluation into a Staged Programming Language},

2343 year = {1998},

2344 author = {Tim Sheard}

2347@inproceedings{nbe2,

2348 title = {Normalization by evaluation},

2349 year = {1998},

2350 author = {Ulrich Berger and Matthias Eberl and Helmut Schwichtenberg},

2351 booktitle = {Prospects for Hardware Foundations 1998},

2352 pages = {117--137},

2353 series = {LNCS}

2358@misc{rtcg_jfp,

2359 title = {Compiling for Run-time Code Generation},

2360 year = {2000},

2361 author = {Frederick Smith and Dan Grossman and Greg Morrisett and Luke Hornof and Trevor J},

2362 note = {Under consideration for J. Functional Programming}

2365@phdthesis{fredsmith_thesis,

2366 month = {January},

2367 school = {Cornell University},

2368 title = {Certified Run-time Code Generation},

2369 year = {2002},

2370 author = {Frederick Smith}

2373@inproceedings{xi_arraybounds,

2374author = "Hongwei Xi and Frank Pfenning",

2375title = {Eliminating Array Bound Checking through Dependent Types},

2376booktitle = "Proceedings of {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation",

2377year = 1998,

2378month = "June",

2379address = "Montreal",

2380pages = "249--257",

2383@inproceedings{xi_deadcode,

2384author = "Hongwei Xi",

2385title = {Dead Code Elimination through Dependent Types},

2386booktitle = "The First International Workshop on Practical Aspects of Declarative Languages",

2387year = 1999,

2388month = "January",

2389address = "San Antonio",

2390pages = "228--242"

2393@book{compilers,

2394 title = {Compilers --- Principles, Techniques and Tools},

2395 year = {1986},

2396 publisher = {Addison-Wesley},

2397 author = {Alfred Aho and Ravi Sethi and Jeffrey Ullman}

2400@inproceedings{nhc,

2401 title = {Highlights from nhc: A space efficient {Haskell} Compiler},

2402 year = {1995},

2403 author = "Niklas R{\"o}jemo",

2404 booktitle = "Functional Programming Languages and Computer Architecture",

2405 pages = "282--292"

2409@misc{mlmatch,

2410 title = {SML/NJ Match Compiler Notes},

2411 year = {1992},

2412 author = {William Aitken}

2415@misc{mlmatch_sestoft,

2416 title = {ML pattern match compilation and partial evaluation},

2417 year = {1992},

2418 author = {Peter Sestoft}

2421@inproceedings{compiledstrongreduction,

2422 title = {A Compiled Implementation of Strong Reduction},

2423 year = {2002},

2424 author = {Benjamin Gr\'{e}goire and Xavier Leroy},

2425 booktitle = {Proc. 2002 International Conf. on Functional Programming ({ICFP} 2002)},

2426 pages = {235--246}

2429@misc{tclhaskell,

2430 howpublished = {http://www.dcs.gla.ac.uk/~meurig/TclHaskell/usermanual.html},

2431 month = {August},

2432 title = {TclHaskell - User Manual},

2433 year = {1999},

2434 author = {Meurig Sage}

2438@InProceedings{nbe-cat,

2439 author = "Thorsten Altenkirch and Martin Hofmann and Thomas Streicher",

2440 title = "Categorical reconstruction of a reduction free

2441 normalization proof",

2442 year = "1995",

2443 booktitle = "Category Theory and Computer Science",

2444 editor = {David Pitt and David E. Rydeheard and Peter Johnstone},

2445 series = {LNCS},

2446 volume = {953},

2447 pages = {182-199}

2450@inproceedings{presburgerEFSM,

2451 title = {A Comparison of Presburger Engines for EFSM Reachability},

2452 year = {1998},

2453 booktitle = {Computer Aided Verification '98},

2454 pages = {280--292},

2455 author = {Thomas R. Shiple and James H. Kukula and Rajeev K. Ranjan}

2458@misc{typesafecast,

2459 title = {Type-Safe Cast},

2460 year = {2000},

2461 author = {Stephanie Weirich}

2464@phdthesis{grobauer-thesis,

2465 school = {University of Aarhus},

2466 title = {Topics in Semantics Based Program Manipulation},

2467 year = {2001},

2468 author = {Bernd Grobauer}

2471@misc{monads-moggi,

2472 title = {Computational Lambda Calculus and Monads},

2473 year = {1989},

2474 author = {Eugenio Moggi}

2477@article{gmp-proof,

2478 title = {A proof of {GMP} square root},

2479 year = {2002},

2480 journal = {Journal of Automated Reasoning},

2481 volume = {29},

2482 pages = {225--252},

2483 author = {Yves Bertot and Nicolas Magaud and Paul Zimmerman}

2486@article{F-tal,

2487 journal = {{ACM} Transactions on Programming Languages and Systems},

2488 number = {3},

2489 month = {May},

2490 volume = {21},

2491 title = {From {System F} to Typed Assembly Language},

2492 year = {1999},

2493 pages = {528--569},

2494 author = {Greg Morrisett and David Walker and Karl Crary and Neal Glew}

2497@techreport{nbe-rtcg,

2498 month = {December},

2499 title = {Strong Normalization by Type-Directed Partial Evaluation and Run-Time Code Generation},

2500 year = {1997},

2501 institution = {BRICS},

2502 author = {Vincent Balat and Oliver Danvy}

2505@misc{yong-schemata,

2506 howpublished = {http://www.dur.ac.uk/yong.luo/},

2507 title = {A Methodology for Implementing Inductive Schemata},

2508 year = {2002},

2509 author = {Yong Luo and Zhaohui Luo}

2512@inproceedings{harper93,

2513 title = {Explicit Polymorphism and CPS Conversion},

2514 year = {1993},

2515 booktitle = {20th {ACM} {SIGPLAN}-SIGACT Symposium on Principles of Programming Languages},

2516 pages = {206--219},

2517 publisher = {{ACM} Press, New York, NY, USA},

2518 author = {Robert Harper and Mark Lillibridge}

2521@techreport{backends,

2522 month = {November},

2523 title = {Functional Back-Ends within the Lambda-Sigma Calculus},

2524 year = {1996},

2525 institution = {INRIA},

2526 author = {Th\'{e}r\`{e}se Hardin and Luc Maranget and Bruno Pagano}

2529@article{stg,

2530 title = {Implementing lazy functional languages on stock hardware -- the {Spineless Tagless G-machine}},

2531 year = {1992},

2532 journal = {Journal of Functional Programming},

2533 volume = {2},

2534 number = {2},

2535 pages = {127--202},

2536 month = {April},

2537 author = {Simon {Peyton Jones}}

2540@article{debruijn,

2541 journal = {Indagationes Mathematicae},

2542 volume = {34},

2543 title = {Lambda calculus notation with nameless dummies},

2544 year = {1972},

2545 pages = {381--392},

2546 author = {N.G. de Bruijn}

2549@book{assembly,

2550 month = {January},

2551 title = {PC Assembly Language},

2552 year = {2002},

2553 publisher = {http://www.drpaulcarter.com/},

2554 author = {Paul A. Carter}

2557@inproceedings{poly99,

2558 title = {Once Upon A Polymorphic Type},

2559 year = {1999},

2560 booktitle = {26th {ACM} {SIGPLAN}-SIGACT Symposium on Principles of Programming Languages},

2561 publisher = {{ACM}},

2562 author = {Keith Wansbrough and Simon {Peyton Jones}}

2565@misc{lazy_intro,

2566 title = {Compiling Lazy Functional Languages: An introduction},

2567 year = {1986},

2568 author = {Thomas Johnsson}

2571@inproceedings{unboxed-fp,

2572 month = {Sept},

2573 title = {Unboxed Values as First Class Citizens in a Non-Strict Functional Language},

2574 year = {1991},

2575 author = {Simon {Peyton Jones} and John Launchbury},

2576 booktitle = {Functional Programming Languages and Computer Architecture (FPCA'91)},

2577 crossref = {fplca91},

2578 pages = {636--666}

2581@inproceedings{abc-machine,

2582 author = {Sjaak Smetsers and Eric N{\"{o}}cker and John {van Groningen} and Rinus Plasmeijer},

2583 title = {Generating efficient code for lazy functional languages},

2584 booktitle = {Functional programming Languages and Computer Architecture},

2585 year = {1991},

2586 pages = {592--617},

2587 crossref = {fplca91}

2590@proceedings{fplca91,

2591 title = {Functional programming Languages and Computer Architecture},

2592 year = {1991},

2593 volume = {523},

2594 series = {LNCS},

2595 publisher = {Springer-Verlag},

2596 editor = {John Hughes}

2601@inproceedings{nbe,

2602 title = {An inverse of the evaluation functional for typed $\lambda$-calculus},

2603 year = {1991},

2604 booktitle = {Proc. 1991 {IEEE} Symp. on Logic in Comp. Sci.},

2605 pages = {203--211},

2606 editor = {R. Vemuri},

2607 author = {Ulrich Berger and Helmut Schwichtenberg}

2610@inproceedings{typed-closure,

2611 title = {Typed Closure Conversion},

2612 year = {1996},

2613 booktitle = {Symposium on Principles of Programming Languages},

2614 pages = {271--283},

2615 author = {Yasuhiko Minamide and J. Gregory Morrisett and Robert Harper}

2618@misc{ghc-commentary,

2619 howpublished = {http://www.cse.unsw.edu.au/~chak/haskell/ghc/comm/},

2620 title = {The Glasgow Haskell Compiler (GHC) Commentary},

2621 year = {2002},

2622 author = {Manuel M. T. Chakravarty and Sigbjorn Finne and Simon Marlow and Simon {Peyton Jones} and Julian Seward and Reuben Thomas},

2623 note = {Available from GHC CVS repository}

2626@inproceedings{lambdalift,

2627 month = {September},

2628 title = {Lambda Lifting: Transforming Programs to Recursive Equations},

2629 year = {1985},

2630 booktitle = {Functional Programming Languages and Computer Architecture},

2631 pages = {190--203},

2632 editor = {Jean-Pierre Jouannaud},

2633 publisher = {Springer-Verlag},

2634 author = {Thomas Johnsson}

2637@inproceedings{til,

2638 title = {TIL: A Type-Directed Optimizing Compiler for ML},

2639 year = {1996},

2640 booktitle = {Proc. {{ACM}} {{SIGPLAN}} '96 Conference on Programming Language Design and Implementation},

2641 pages = {181--192},

2642 author = {D. Tarditi and G. Morrisett and P. Cheng and C. Stone and R. Harper and P. Lee}

2645@phdthesis{shao94,

2646 school = {Princeton University},

2647 title = {Compiling Standard {ML} for Efficient Execution on Modern Machines},

2648 year = {1994},

2649 author = {Zhong Shao}

2652@inproceedings{gmachine,

2653 month = {September},

2654 title = {The {G-Machine}: A fast, graph-reduction evaluator},

2655 year = {1985},

2656 booktitle = {Functional Programming Languages and Computer Architecture},

2657 pages = {400--413},

2658 editor = {Jean-Pierre Jouannaud},

2659 publisher = {Springer-Verlag},

2660 author = {R.B. Kieburtz}

2663@inproceedings{strictness,

2664 month = {September},

2665 title = {Strictness Analysis - A practical approach},

2666 year = {1985},

2667 booktitle = {Functional Programming Languages and Computer Hardware},

2668 pages = {35--49},

2669 editor = {Jean-Pierre Jouannaud},

2670 publisher = {Springer-Verlag},

2671 author = {Chris Clack and Simon {Peyton Jones}}

2674@book{fl-impl,

2675 title = {Implementing Functional Languages - A Tutorial},

2676 year = {1992},

2677 publisher = {Prentice Hall International},

2678 author = {Simon {Peyton Jones} and David Lester}

2681@phdthesis{capretta-thesis,

2682 school = {Katholieke Universiteit Nijmegen},

2683 title = {Abstraction and Computation},

2684 year = {2002},

2685 author = {Venanzio Capretta}

2688@article{bird-pointer,

2689 journal = {Journal of Functional Programming},

2690 number = {3},

2691 month = {May},

2692 volume = {11},

2693 title = {Unfolding Pointer Algorithms},

2694 year = {2001},

2695 pages = {347--358},

2696 author = {Richard S. Bird}

2699@article{impl-tp,

2700 journal = {Journal of Functional Programming},

2701 number = {2},

2702 month = {March},

2703 volume = {9},

2704 title = {Implementing Theorem Provers in a Purely Functional Style},

2705 year = {1999},

2706 pages = {147--166},

2707 author = {Keith Hanna}

2710@article{shrink-lambda,

2711 journal = {Journal of Functional Programming},

2712 number = {5},

2713 month = {September},

2714 volume = {7},

2715 title = {Shrinking Lambda Expressions in Linear Time},

2716 year = {1997},

2717 pages = {515--540},

2718 author = {Andrew W. Appel and Trevor Jim}

2721@article{stack-tal,

2722 journal = {Journal of Functional Programming},

2723 number = {1},

2724 month = {January},

2725 volume = {12},

2726 title = {Stack-based Typed Assembly Language},

2727 year = {2002},

2728 pages = {43--88},

2729 author = {Greg Morrisset and Karl Crart and Neal Glew and David Walker}

2732@article{runtime-lamsig,

2733 journal = {Journal of Functional Programming},

2734 number = {2},

2735 month = {March},

2736 volume = {8},

2737 title = {Functional Runtime Systems within the lambda-sigma Calculus},

2738 year = {1998},

2739 pages = {131--176},

2740 author = {Th\'{e}r\`{e}se Hardin and Luc Maranget and Bruno Pagano}

2743@article{busylazy,

2744 journal = {Journal of Functional Programming},

2745 number = {6},

2746 month = {November},

2747 volume = {11},

2748 title = {How to look busy while being as lazy as ever: the Implementation of a lazy functional debugger},

2749 year = {2001},

2750 pages = {629--671},

2751 author = {Henrik Nilsson}

2754@article{lazyveager,

2755 journal = {Journal of Functional Programming},

2756 number = {5},

2757 month = {September},

2758 volume = {7},

2759 title = {More haste, less speed: lazy versus eager evaluation},

2760 year = {1997},

2761 pages = {541--547},

2762 author = {Richard Bird and Geraint Jones and Oege {de Moor}}

2765@article{jvm-fp,

2766 journal = {Journal of Functional Programming},

2767 number = {6},

2768 month = {November},

2769 volume = {9},

2770 title = {Compiling lazy functional programs for the Java Virtual Machine},

2771 year = {1999},

2772 pages = {579--603},

2773 author = {David Wakeling}

2776@book{isabelle,

2777 publisher = {Springer-Verlag},

2778 series = {LNCS},

2779 volume = {2283},

2780 month = {March},

2781 title = {Isabelle/HOL - A proof assistant for higher order logic},

2782 year = {2002},

2783 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}

2786@article{ghc-inliner,

2787 journal = {Journal of Functional Programming},

2788 number = {4},

2789 month = {September},

2790 volume = {12},

2791 title = {Secrets of the {Glasgow Haskell Compiler} inliner},

2792 year = {2002},

2793 pages = {393--434},

2794 author = {Simon {Peyton Jones} and Simon Marlow}

2797@article{dynamic-fp,

2798 journal = {Journal of Functional Programming},

2799 number = {1},

2800 month = {January},

2801 volume = {8},

2802 title = {The dynamic compiliation of lazy functional programs},

2803 year = {1998},

2804 pages = {61--81},

2805 author = {David Wakeling}

2808@misc{isabelle-ref,

2809 month = {March},

2810 title = {Isabelle Reference Manual},

2811 year = {2002},

2812 author = {Lawrence C. Paulson}

2815@article{debruijn-nested,

2816 journal = {Journal of Functional Programming},

2817 number = {1},

2818 month = {January},

2819 volume = {9},

2820 title = {de Bruijn notation as a nested datatype},

2821 year = {1999},

2822 pages = {77--91},

2823 author = {Richard S. Bird and Ross Paterson}

2826@article{perfect-trees,

2827 journal = {Journal of Functional Programming},

2828 number = {3},

2829 month = {May},

2830 volume = {10},

2831 title = {Perfect trees and bit-reversal permutations},

2832 year = {2000},

2833 pages = {305--317},

2834 author = {Ralf Hinze}

2837@phdthesis{paulin-extraction,

2838 school = {Paris 7},

2839 title = {Extraction de programmes dans le Calcul des Constructions},

2840 year = {1989},

2841 author = {Christine Paulin-Mohring}

2844@phdthesis{santos95,

2845 school = {University of Glasgow},

2846 title = {Compilation By Transformation In Non-Strict Functional Languages},

2847 year = {1995},

2848 author = {{Andr\'{e} Lu\'{i}s de Medeiros} Santos}

2851@book{cps,

2852 title = {Compiling With Continuations},

2853 year = {1992},

2854 publisher = {Cambridge University Press},

2855 author = {Andrew W. Appel}

2858@techreport{SKIM,

2859 number = {31},

2860 title = {The {SKIM} microprogrammer's guide},

2861 year = {1983},

2862 institution = {University of Cambridge},

2863 author = {W.R. Stoye}

2866@misc{NORMA,

2867 title = {An Overview of Burroughs {NORMA}},

2868 year = {1985},

2869 author = {H. Richards}

2872@book{ml,

2873 title = {The Definition of Standard ML --- Revised},

2874 year = {1997},

2875 publisher = {MIT Press},

2876 author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen}

2879@misc{ml71,

2880 title = {An intuitionistic theory of types},

2881 year = {1971},

2882 author = {Per Martin-L\"{o}f}

2885@phdthesis{girard-thesis,

2886 school = {Universit\'{e} Paris VII},

2887 title = {Interpr\'{e}tation fonctionelle et \'{e}limination des coupures de l'arithm\'{e}tique d'ordre sup\'{e}rieur},

2888 year = {1972},

2889 author = {Jean-Yves Girard}

2892@inproceedings{ml75,

2893 title = {An intuitionistic theory of types: predicative part},

2894 year = {1975},

2895 booktitle = {Logic Colloquium '73},

2896 editor = {H. Rose and J.C. Shepherdson},

2897 publisher = {North-Holland},

2898 author = {Per Martin-L\"{o}f}

2901@inproceedings{cpm90,

2902 title = {Inductively defined types},

2903 year = {1990},

2904 author = {Thierry Coquand and Christine Paulin-Mohring},

2905 series = {LNCS},

2906 volume = {417},

2907 publusher = {Springer-Verlag}

2910@phdthesis{fpcustom,

2911 month = {May},

2912 school = {Computer Lab, University of Cambridge},

2913 title = {The Implementation of Functional Languages using Custom Hardware},

2914 year = {1985},

2915 author = {W.R. Stoye}

2918@phdthesis{hughesthesis,

2919 month = {September},

2920 school = {Programming Research Group, Oxford},

2921 title = {The design and implementation of programming languages},

2922 year = {1984},

2923 author = {John Hughes}

2926@inproceedings{tim,

2927 volume = {274},

2928 title = {{TIM} -- A simple lazy abstract machine to execute supercombinators},

2929 year = {1987},

2930 booktitle = {Functional Programming Languages and Computer Architecture},

2931 publisher = {Springer-Verlag},

2932 author = {John Fairbairn and Stuart Wray},

2933 pages = {34--45},

2934 series = {LNCS}

2937@techreport{abc,

2938 title = {The {ABC} machine -- A Sequential Stack-based Abstract Machine For Graph Rewriting},

2939 year = {1990},

2940 institution = {University of Nijmegen},

2941 author = {P.W.M. Koopman and M.C.J.D. van {Eekelen} and E.G.J.M.H. Ncker and J.E.W. Smetsers and M.J. Plasmeijer}

2944@techreport{implicit,

2945 title = {On Implicit Arguments},

2946 year = {1994},

2947 institution = {Faculty of Science, University of Tokyo},

2948 author = {Masami Hagiya and Yozo Toda}

2951@book{semantics,

2952 title = {Denotational Semantics},

2953 year = {1986},

2954 publisher = {Wm. C. Brown},

2955 author = {David A. Schmidt}

2958@inproceedings{lazyml,

2959 month = {August},

2960 title = {A compiler for {Lazy} {ML}},

2961 year = {1984},

2962 booktitle = {Proceedings of the {{ACM}} Symposium on Lisp and Functional Programming},

2963 pages = {218--227},

2964 author = {Lennart Augustsson}

2967@inproceedings{nu-g,

2968 title = {Parallel graph reduction with the $\langle\nu,G\rangle$-machine},

2969 year = {1989},

2970 booktitle = {Functional Programming Languages and Computer Architecture},

2971 publisher = {{ACM} Press},

2972 author = {Lennart Augustsson and Thomas Johnsson}

2975@book{k&r,

2976 title = {The C programming language},

2977 year = {1988},

2978 publisher = {Prentice-Hall},

2979 author = {Brian W. Kernighan and Dennis M. Ritchie}

2982@misc{c--garbage,

2983 title = {C--: a portable assembly language that supports garbage collection},

2984 year = {1999},

2985 author = {Simon {Peyton Jones} and Norman Ramsey and Fermin Reig},

2986 note = {Invited talk at PPDP'99}

2989@misc{epigram,

2990 howpublished = {http://www.dur.ac.uk/CARG/epigram.html},

2991 title = {Project Proposal: {Epigram}: Innovative Programming via Inductive Families},

2992 year = {2002},

2993 author = {Zhaohui Luo and James McKinna and Paul Callaghan and Conor McBride}

2996@misc{ghc-rewrite,

2997 title = {Playing by the Rules: Rewriting as a practical optimisation technique in {GHC}},

2998 year = {2001},

2999 author = {Simon {Peyton Jones} and Andrew Tolmach and Tony Hoare}

3002@UNPUBLISHED{implicit-pollack,

3003 AUTHOR = {Robert Pollack},

3004 TITLE = {Implicit Syntax},

3005 NOTE = {Informal Proceedings of First Workshop on

3006 Logical Frameworks, Antibes},

3007 YEAR = {1990},

3008 MONTH = MAY

3012@article{transform-haskell,

3013 journal = {Science of Computer Programming},

3014 volume = {32},

3015 title = {A transformation-based optimiser for {Haskell}},

3016 year = {1998},

3017 pages = {3--47},

3018 author = {Simon {Peyton Jones} and Andr\'{e} L. M. Santos}

3021@inproceedings{knuth-bendix,

3022 title = {Simple Word Problems in Universal Algebras},

3023 year = {1970},

3024 booktitle = {Computational Problems in Abstract Algebra},

3025 pages = {263--298},

3026 editor = {John Leech},

3027 publisher = {Pergamon Press},

3028 author = {Donald E. Knuth and Peter B. Bendix}

3031@inproceedings{phantomfun,

3032 title = {Fun With Phantom Types},

3033 author = {Ralf Hinze},

3034 pages = {245--262},

3035 year = {2003},

3036 crossref = {funprogramming},

3037 booktitle = {The Fun Of Programming},

3038 publisher = {Palgrave}

3041@book{funprogramming,

3042 month = {March},

3043 title = {The Fun Of Programming},

3044 year = {2003},

3045 editor = {Jeremy Gibbons and Oege {de Moor}},

3046 publisher = {Palgrave},

3047 series = {Cornerstones of Computing}

3050@inproceedings{anderson-proof,

3051 title = {Representing Proof Transformations For Program Optimization},

3052 year = {1994},

3053 booktitle = {International Conference On Automated Deduction},

3054 publisher = {Springer Verlag},

3055 author = {Penny Anderson}

3058@phdthesis{daria-thesis,

3059 month = {April},

3060 school = {Institute of Informatics, Warsaw University},

3061 title = {Termination of Rewriting in the Calculus of Constructions},

3062 year = {2003},

3063 author = {Daria Walukiewicz-Chrzaszcz}

3066@inproceedings{change-data,

3067 title = {Changing Data Structures In Type Theory: A Study Of Natural Numbers},

3068 year = {2001},

3069 booktitle = {Types For Proofs And Programs 2000},

3070 pages = {181--196},

3071 editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},

3072 publisher = {Springer},

3073 author = {Nicolas Magaud and Yves Bertot}

3076@phdthesis{nico-thesis,

3077 title = {Changement de Representation des donn\'{e}es dans le Calcul de Constructions},

3078 author = {Nicolas Magaud},

3079 year = {2003},

3080 month = {October},

3081 school = {Universit\'{e} de Nice - Sophia Antipolis}

3085@book{patterns,

3086 title = {Design Patterns},

3087 year = {1995},

3088 publisher = {Addison Wesley},

3089 author = {Erich Gamma and Richard Helm and Ralph Johnson and John Vlissides}

3092@misc{ghchugs,

3093 month = {August},

3094 title = {The New {GHC}/{Hugs} Runtime System},

3095 year = {1998},

3096 author = {Simon Marlow and Simon {Peyton Jones}}

3099@misc{stgrevised,

3100 month = {February},

3101 title = {The {STG} runtime system (revised)},

3102 year = {1999},

3103 author = {Simon {Peyton Jones} and Simon Marlow and Alastair Reid},

3104 howpublished = {Available from \verb+http://www.haskell.org/ghc/documentation.html+}

3107@inproceedings{optimistic,

3108 month = {March},

3109 title = {Optimistic Evaluation --- an adaptive evaluation strategy for non-strict programs},

3110 year = {2003},

3111 author = {Robert Ennals and Simon {Peyton Jones}},

3112 booktitle = {International Conference on Functional Programming},

3113 pages = {287--298}

3116@phdthesis{ennals-thesis,

3117 title = {Adaptive Evaluation of Non-Strict Programs},

3118 author = {Robert Ennals},

3119 year = {2003},

3120 month = {December},

3121 school = {King's College, University of Cambridge}

3124@article{garbage,

3125 journal = {{ACM} Computing Surveys},

3126 number = {3},

3127 volume = {13},

3128 title = {Garbage Collection of Linked Data Structures},

3129 year = {1981},

3130 pages = {341--367},

3131 author = {Jacques Cohen}

3134@article{baker-gc,

3135 journal = {Communications of the {ACM}},

3136 number = {4},

3137 month = {April},

3138 volume = {21},

3139 title = {List Processing In Real Time On A Serial Computer},

3140 year = {1978},

3141 pages = {280--294},

3142 author = {Henry G. {Baker Jr}}

3145@misc{bc-rec,

3146 month = {February},

3147 title = {Modelling General Recursion in Type Theory},

3148 year = {2003},

3149 note = {Under consideration for publication in Math. Struct. in Comp. Science. Draft, DCS, CTH --- INRIA, Sophia Antipolis, France},

3150 author = {Ana Bove and Venanzio Capretta}

3153@misc{global-tag,

3154 title = {Global Tagging Optimization by Type Inference},

3155 year = {1992},

3156 author = {Fritz Henglein}

3159@book{esr,

3160 month = {October},

3161 title = {The Cathedral And The Bazaar},

3162 year = {1999},

3163 publisher = {O'Reilly},

3164 author = {Eric Raymond}

3167@book{manmonth,

3168 title = {The Mythical Man-month: Essays on Software Engineering},

3169 year = {1975},

3170 publisher = {Addison Wesley},

3171 author = {Frederick P. Brooks}

3174@inproceedings{evalpush,

3175 title = {How to make a fast curry: push/enter vs eval/apply},

3176 year = {2004},

3177 author = {Simon Marlow and Simon {Peyton Jones}},

3178 booktitle = {International Conference on Functional Programming, Snowbird},

3179 pages = {4--15}

3182@phdthesis{boquist-thesis,

3183 month = {April},

3184 school = {Chalmers University of Technology},

3185 title = {Code Optimisation Techniques for Lazy Functional Languages},

3186 year = {1999},

3187 author = {Urban Boquist}

3190@book{formal-spec,

3191 title = {Formal Specification Of Programming Languages},

3192 year = {1981},

3193 publisher = {Prentice-Hall},

3194 author = {Frank G. Pagan}

3197@inproceedings{elim-motive,

3198 title = {Elimination With A Motive},

3199 year = {2000},

3200 booktitle = {Types for Proofs and Programs},

3201 pages = {197--216},

3202 editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},

3203 publisher = {Springer},

3204 author = {Conor McBride}

3207@article{telescope,

3208 journal = {Information and Computation},

3209 number = {2},

3210 month = {April},

3211 volume = {91},

3212 title = {Telescoping Mappings in Typed Lambda Calculus},

3213 year = {1991},

3214 pages = {189--204},

3215 author = {N.G. de Bruijn}

3218@misc{typeintype,

3219 title = {Typechecking is undecidable when 'type' is a type},

3220 year = {1989},

3221 author = {Mark B. Reinhold}

3224@misc{core,

3225 month = {September},

3226 title = {An External Representation for the {GHC} Core Language},

3227 year = {2001},

3228 author = {Andrew Tolmach and {The GHC Team}}

3231@article{deforestation,

3232 journal = {Theoretical Computer Science},

3233 volume = {73},

3234 title = {Deforestation: Transforming programs to eliminate trees},

3235 year = {1990},

3236 pages = {231--248},

3237 author = {Philip Wadler}

3240@misc{hep,

3241 month = {July},

3242 title = {Architecture of the {Haskell} Execution Platform},

3243 year = {1999},

3244 author = {Julian Seward and Simon Marlow and Andy Gill and Sigbjorn Finne and Simon {Peyton Jones} },

3245 note = {Version 6},

3246 howpublished = {Available from \verb+http://www.haskell.org/ghc/documentation.html+}

3249@mastersthesis{wahlstedt-thesis,

3250 month = {October},

3251 school = {Chalmers University Of Technology},

3252 title = {Detecting Termination Using Size Change In Parameter Values},

3253 year = {2000},

3254 author = {David Wahlstedt}

3257@inproceedings{size-change,

3258 title = {The size-change principle for program termination},

3259 year = {2001},

3260 booktitle = {Proceedings of the 28th Annual {ACM} {SIGPLAN}-SIGACT Symposium on Principles of Programming Languages},

3261 author = {Chin Soon Lee and Neil D. Jones and Amir Ben-Amram. }

3264@article{ski-turner,

3265 journal = {Software -- Practice and Experience},

3266 volume = {9},

3267 title = {A new implementation technique for applicative languages},

3268 year = {1979},

3269 pages = {31--49},

3270 author = {David Turner}

3273@inproceedings{turner-strong,

3274 number = {1022},

3275 title = {Elementary Strong Functional Programming},

3276 year = {1996},

3277 booktitle = {First International Symposium on Functional Programming Languages in Education, Nijmegen, Netherlands, December 1995.},

3278 pages = {1--13},

3279 publisher = {Springer},

3280 author = {David Turner},

3281 series = {LNCS}

3284@misc{clean,

3285 title = {The {Concurrent CLEAN} Language Report (draft)},

3286 year = {2003},

3287 author = {Rinus Plasmeijer and Marko van Eekelen},

3288 howpublished = {Available from \verb+http://www.cs.kun.nl/~clean/+}

3291@article{burstall-struct,

3292 journal = {Computer Journal},

3293 number = {1},

3294 volume = {12},

3295 title = {Proving Properties of Programs By Structural Induction},

3296 year = {1969},

3297 pages = {41--48},

3298 author = {Rod Burstall}

3301@incollection{ barendregt-types,

3302 author = "Henk Barendregt",

3303 title = "Lambda Calculi with Types",

3304 booktitle = "Handbook of Logic in Computer Science, Volumes 1 (Background: Mathematical Structures) and 2 (Background: Computational Structures), Abramsky \& Gabbay \& Maibaum (Eds.)",

3305 publisher = "Clarendon",

3306 volume = "2",

3307 year = "1992",

3308 url = "citeseer.nj.nec.com/barendregt92lambda.html" }

3310@book{curry-feys,

3311 title = {Combinatory Logic, volume 1},

3312 year = {1958},

3313 publisher = {North Holland},

3314 author = {Haskell B. Curry and Robert Feys}

3317@phdthesis{bove-thesis,

3318 month = {November},

3319 school = {Chalmers University of Technology},

3320 title = {General Recursion in Type Theory},

3321 year = {2002},

3322 author = {Ana Bove}

3325@inbook{ml-cm,

3326 title = {Constructive Mathematics and Computer Programming},

3327 year = {1985},

3328 booktitle = {Mathematical Logic and Programming Languages},

3329 publisher = {Prentice Hall},

3330 author = {Per Martin-L\"{o}f}

3333@inproceedings{howard,

3334 title = {The formulae-as-types notion of construction},

3335 year = {1980},

3336 booktitle = {To H.B.Curry: Essays on combinatory logic, lambda calculus and formalism},

3337 editor = {Jonathan P. Seldin and J. Roger Hindley},

3338 publisher = {Academic Press},

3339 author = {William A. Howard},

3340 note = {A reprint of an unpublished manuscript from 1969}

3343@inproceedings{talx86,

3344 title = {TALx86: A Realistic Typed Assembly Language},

3345 year = {1999},

3346 booktitle = {{ACM} {SIGPLAN} Workshop on Compiler Support for System Software},

3347 pages = {25--35},

3348 author = {Greg Morrisett and Karl Crary and Neal Glew and Dan Grossman and Richard Samuels and Frederick Smith and David Walker and Stephanie Weirich and Steve Zdancewic}

3351@inproceedings{bove-capretta,

3352 volume = {2152},

3353 title = {Nested General Recursion and Partiality in Type Theory},

3354 year = {2001},

3355 booktitle = {Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLS 2001},

3356 pages = {121--135},

3357 editor = {Richard J. Boulton and Paul B. Jackson},

3358 publisher = {Springer-Verlag},

3359 author = {Ana Bove and Venanzio Capretta},

3360 series = {LNCS}

3363@misc{lvm,

3364 month = {November},

3365 title = {LVM, the lazy virtual machine},

3366 year = {2002},

3367 author = {Daan Leijen}

3370@misc{ocaml,

3371 howpublished = {\verb+http://caml.inria.fr/ocaml/htmlman/+},

3372 month = {August},

3373 title = {The {Objective Caml} system release 3.06},

3374 year = {2002},

3375 author = {Xavier Leroy}

3378@misc{lambdagoto,

3379 title = {Lambda : The Ultimate Goto},

3380 year = {1977},

3381 author = {Guy L. {Steele Jr}},

3382 note = {MIT AI Memo 443}

3385@inproceedings{ liu-tail,

3386 author = "Yanhong A. Liu and Scott D. Stoller",

3387 title = "From Recursion to Iteration: What are the Optimizations?",

3388 booktitle = "Partial Evaluation and Semantic-Based Program Manipulation",

3389 pages = "73-82",

3390 year = "2000",

3391 url = "citeseer.nj.nec.com/liu00from.html" }

3393@inproceedings{aczel77,

3394 title = {An Introduction To Inductive Definitions},

3395 year = {1977},

3396 booktitle = {Handbook of Mathematical Logic},

3397 editor = {J. Barwise},

3398 publisher = {North Holland},

3399 author = {Peter Aczel}

3402@inproceedings{inductive-plastic,

3403 volume = {1956},

3404 title = {Implementation Techniques for Inductive Types in {Plastic}},

3405 year = {1999},

3406 booktitle = {Types for Proofs and Programs},

3407 pages = {94--113},

3408 editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr\"{o}m and Jan Smith},

3409 publisher = {Springer-Verlag},

3410 author = {Paul Callaghan and Zhaohui Luo},

3411 series = {LNCS}

3414@misc{graham,

3415 howpublished = {Available from \verb+http://www.paulgraham.com/+},

3416 month = {April},

3417 title = {The Hundred Year Language},

3418 year = {2003},

3419 author = {Paul Graham},

3420 note = {Keynote address at PyCon 2003}

3423@inproceedings{gimenez98,

3424 volume = {1443},

3425 title = {Structural Recursive Definitions in Type Theory},

3426 year = {1998},

3427 booktitle = {Proceedings of ICALP '98},

3428 publisher = {Springer-Verlag},

3429 author = {Eduardo Gim\'{e}nez},

3430 series = {LNCS}

3433@article{quicksort,

3434 journal = {Computer Journal},

3435 number = {1},

3436 volume = {5},

3437 title = {Quicksort},

3438 year = {1962},

3439 pages = {10--15},

3440 author = {C.A.R. Hoare}

3443@phdthesis{goguen-thesis,

3444 school = {University of Edinburgh},

3445 title = {A Typed Operational Semantics for Type Theory},

3446 year = {1994},

3447 author = {Healfdene Goguen}

3450@article{ph-universes,

3451 journal = {Theoretical Computer Science},

3452 number = {1},

3453 volume = {89},

3454 title = {Type Checking With Universes},

3455 year = {1991},

3456 pages = {107--136},

3457 author = {Robert Harper and Randy Pollack}

3460@inproceedings{pm-compile,

3461 month = {September},

3462 title = {Compiling Pattern Matching},

3463 year = {1985},

3464 booktitle = {Functional Programming Languages and Computer Architecture},

3465 pages = {368--381},

3466 editor = {Jean-Pierre Jouannaud},

3467 publisher = {Springer-Verlag},

3468 author = {Lennart Augustsson}

3471@phdthesis{lena-thesis,

3472 school = {Chalmers University of Technology, G\"{o}teborg},

3473 title = {The implementation of {ALF} -- A Proof Editor based on {Martin-L\"{o}f}'s Monomorphic Type Theory with Explicit Substitutions},

3474 year = {1994},

3475 author = {Lena Magnusson}

3478@article{view-left,

3479 journal = {Journal of Functional Programming},

3480 number = {1},

3481 volume = {14},

3482 title = {The View From The Left},

3483 year = {2004},

3484 author = {Conor McBride and James McKinna},

3485 pages = {69--111}

3488@inproceedings{not-a-number,

3489 author = {Conor McBride and James McKinna},

3490 title = {I am not a number, {I} am a free variable},

3491 year = {2004},

3492 booktitle = {Proceedings of the {ACM} {SIGPLAN} Haskell Workshop}

3496@misc{profiling,

3497 title = {Time and Space Profiling for Non-Strict, Higher Order Functional Languages},

3498 year = {1995},

3499 author = {Patrick M. Sansom and Simon {Peyton Jones}}

3502@inbook{pattern-matching,

3503 title = {The Implementation of Functional Programming Languages},

3504 year = {1987},

3505 booktitle = {The Implementation of Functional Programming Languages},

3506 pages = {78--103},

3507 editor = {Simon {Peyton Jones}},

3508 chapter = {5},

3509 publisher = {Prentice Hall},

3510 author = {Philip Wadler},

3511 crossref = {pj-imp}

3514@article{pe-problems,

3515 author = {Jones, N. D.},

3516 title = {Challenging problems in partial evaluation and mixed computation},

3517 journal = {New Gen. Comput.},

3518 volume = {6},

3519 number = {2-3},

3520 year = {1988},

3521 issn = {0288-3635},

3522 pages = {291--302},

3523 doi = {http://dx.doi.org/10.1007/BF03037143},

3524 publisher = {Ohmsha},

3525 address = {Tokyo, Japan, Japan},

3528@inproceedings{tag-elim,

3529 title = {Tag Elimination -- or -- Type Specialisation is a Type Indexed Effect},

3530 year = {2000},

3531 booktitle = {Subtyping and Dependent Types in Programming, APPSEM Workshop},

3532 author = {Walid Taha and Henning Makholm}

3535@inproceedings{extraction-coq,

3536 title = {A New Extraction for {Coq}},

3537 year = {2002},

3538 booktitle = {Types for proofs and programs},

3539 editor = {Herman Geuvers and Freek Wiedijk},

3540 publisher = {Springer},

3541 author = {Pierre Letouzey},

3542 series = {LNCS}

3545@phdthesis{mcbride-snr-thesis,

3546 school = {Queen's University of Belfast},

3547 title = {Computer Aided Manipulation of Symbols},

3548 year = {1970},

3549 author = {Fred McBride}

3552@article{ho-strictness,

3553 journal = {Science of Computer Programming},

3554 volume = {7},

3555 title = {Strictness analysis for higher-order functions},

3556 year = {1986},

3557 pages = {249--278},

3558 author = { Geoffrey L. Burn and Chris Hankin and Samson Abramsky}

3561@phdthesis{mycroft-thesis,

3562 school = {Dept Computer Science, University of Edinburgh},

3563 title = {Abstract interpretation and optimising transformations for applicative programs},

3564 year = {1981},

3565 author = {A. Mycroft}

3568@inproceedings{bc-nested,

3569 month = {September},

3570 volume = {2152},

3571 title = {Nested General Recursion and Partiality in Type Theory},

3572 year = {2001},

3573 booktitle = {Theorem Proving In Higher Order Logics: 14th International Conferences, TPHOLS 2001},

3574 pages = {121--135},

3575 publisher = {Springer--Verlag},

3576 author = {Ana Bove and Venanzio Capretta},

3577 series = {LNCS}

3580@techreport{bove-mutual,

3581 month = {May},

3582 title = {Mutual General Recursion in Type Theory},

3583 year = {2002},

3584 institution = {Department of Computing Science, Chalmers University of Technology},

3585 author = {Ana Bove}

3588@article{berardi-pruning,

3589 journal = {Journal of Logic and Computation},

3590 number = {5},

3591 volume = {6},

3592 title = {Pruning Simply Typed Lambda Terms},

3593 year = {1996},

3594 pages = {663--681},

3595 author = {Stefano Berardi}

3598@article{milner-tc,

3599 journal = {Journal of Computer and System Science},

3600 volume = {17},

3601 title = {A Theory of Type Polymorphism in Programming},

3602 year = {1978},

3603 pages = {348--75},

3604 author = {R. Milner}

3607@inproceedings{extt,

3608 title = {Inductive Families Need Not Store Their Indices},

3609 year = {2004},

3610 booktitle = {Types for Proofs and Programs 2003},

3611 author = {Edwin Brady and Conor McBride and James McKinna},

3612 editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},

3613 series = {Lecture Notes in Computer Science},

3614 publisher = {Springer},

3615 volume = {3085},

3616 pages = {115--129}

3619@book{luo94,

3620 title = {Computation and Reasoning -- A Type Theory for Computer Science},

3621 year = {1994},

3622 publisher = {OUP},

3623 author = {Zhaohui Luo},

3624 series = {Intl. Series of Monographs on Comp. Sci.}

3627@article{backus78,

3628 journal = {Communications of the {ACM}},

3629 month = {August},

3630 volume = {21},

3631 title = {Can Programming Be Liberated From the {Von Neumann} Style?},

3632 year = {1978},

3633 pages = {280--294},

3634 author = {John Backus}

3637@misc{henk,

3638 month = {May},

3639 title = {Henk: A Typed Intermediate Language},

3640 year = {1997},

3641 author = {Simon {Peyton Jones} and Erik Meijer}

3644@article{thunks,

3645 journal = {Journal of Functional Programming},

3646 number = {3},

3647 month = {May},

3648 volume = {7},

3649 title = {Thunks and the $\lambda$-calculus},

3650 year = {1997},

3651 pages = {303--319},

3652 author = {John Hatcliff and Olivier Danvy}

3655@inproceedings{grin-project,

3656 author = "Urban Boquist and Thomas Johnsson",

3657 title = "The {GRIN} Project: A Highly Optimising Back End for Lazy Functional Languages",

3658 booktitle = "Implementation of Functional Languages",

3659 pages = "58--84",

3660 year = "1996",

3661 url = "citeseer.ist.psu.edu/boquist96grin.html" }

3663@misc{boehm-gc,

3664 nothowpublished = {\url{http://www.hpl.hp.com/personal/Hans_Boehm/gc/}},

3665 title = {A garbage collector for {C} and {C++}},

3666 year = {2001},

3667 author = {Hans-J. Boehm and Alan J. Demers and {Xerox Corporation Silicon Graphic} and {Hewlett-Packard Company}}

3670@misc{art-interpreter,

3671 month = {May},

3672 title = {The Art of the Interpreter or, the Modularity Complex (Parts Zero, One, and Two)},

3673 year = {1978},

3674 author = {Guy Lewis {Steele, Jr.} and Gerald Jay Sussman},

3675 note = {MIT AI Lab. AI Lab Memo AIM-453}

3678@inproceedings{gimenez,

3679 title = {Codifying Guarded Definitions With Recursive Schemes},

3680 year = {1994},

3681 booktitle = {Proceedings of TYPES 1994},

3682 pages = {39--59},

3683 author = {Eduardo Gim\'{e}nez}

3686@manual{ghc-manual,

3687 title = {The Glasgow Haskell Compiler User's Guide, Version 6.0},

3688 year = {2003},

3689 author = {The {GHC Team}}

3692@article{rbtree,

3693 journal = {Journal of Functional Programming},

3694 number = {4},

3695 month = {May},

3696 volume = {9},

3697 title = {Red-Black Trees In A Functional Setting},

3698 year = {1999},

3699 pages = {471--477},

3700 author = {Chris Okasaki}

3703@inproceedings{dt-data,

3704author = "Hongwei Xi",

3705title = {{Dependently Typed Data Structures}},

3706booktitle = "Proceedings of Workshop of Algorithmic Aspects of Advanced Programming Languages (WAAAPL '99)",

3707year = 1999,

3708month = "September",

3709pages = "17--32",

3710address = "Paris",

3713@misc{krivine,

3714 title = {On the Correctness and Efficiency of the {Krivine} Machine},

3715 year = {2003},

3716 month = {October},

3717 author = {Mitchell Wand and Daniel P. Friedman},

3718 howpublished = {Submitted for publication}

3719 }

3721@inproceedings{nbe-filinski,

3722 title = {Normalization by Evaluation for the Computational Lambda-Calculus},

3723 year = {2001},

3724 month = {May},

3725 booktitle = {Typed Lambda Calculi and Applications: 5th International Conference, TLCA 2001},

3726 author = {Andrzej Filinski},

3727 pages = {151--165},

3728 publisher = {Springer-Verlag},

3729 series = {LNCS},

3730 volume = {2044}

3733@inproceedings{filinski-nbesem,

3734 title = {A semantic account of type-directed partial evaluation},

3735 year = {1999},

3736 author = {Andrzej Filinski},

3737 editor = {G. Nadathur},

3738 booktitle = {International Conference on Principles and Practice of Declarative Programming},

3739 volume = {1702},

3740 series = {LNCS},

3741 pages = {378--395},

3742 publisher = {Springer-Verlag}

3745@article{secd,

3746 title = {The mechanical evaluation of expressions},

3747 author = {P.J. Landin},

3748 year = {1964},

3749 journal = {Computer Journal},

3750 volume = {6},

3751 pages = {308--320}

3754@misc{lispkit,

3755 title = {The {LispKit} Manual},

3756 author = {Peter Henderson and Geraint Jones and Simon Jones},

3757 year = {1982},

3758 howpublished = {Oxford University Computing Laboratory}

3761@inproceedings{wells-undecidable,

3762 title = {Typability and Type Checking in the Second-order $\lambda$-calculus are equivalent and undecidable},

3763 author = {J. Wells},

3764 year = {1994},

3765 month = {July},

3766 booktitle = {Proc. 9th Ann. {IEEE} Symp. Logic Comput. Sci.}

3769@misc{patguards,

3770 title = {Pattern Guards and Transformational Patterns},

3771 author = {Martin Erwig and Simon {Peyton Jones}},

3772 year = {2000},

3773 howpublished = {Haskell Workshop}

3776@misc{alfa-manual,

3777 title = {Alfa Users' Guide},

3778 author = {Thomas Hallgren},

3779 year = {2001},

3780 howpublished = {Available from \verb+http://www.cs.chalmers.se/~hallgren/Alfa/+}

3783@inproceedings{nofib,

3784 title = {The nofib Benchmark Suite of {Haskell} Programs},

3785 author = {Will Partain},

3786 year = {1992},

3787 booktitle = {Functional Programming},

3788 editor = {J. Launchbury and P.L. Sansom},

3789 series = {Workshops in Computing},

3790 publisher = {Springer Verlag}

3793@article{shape,

3794 title = {Shape in Computing},

3795 author = {Barry Jay},

3796 journal = "{{ACM}} Computing Surveys",

3797 year = "1996",

3798 volume = "28",

3799 number = "2",

3800 pages = "355--357",

3803@misc{ffi,

3804 title = {The {Haskell 98} Foreign Function Interface 1.0: An Addendum to the {Haskell 98} Report},

3805 editor = {Manuel Chakravarty},

3806 key = {FFI},

3807 year = {2002},

3808 month = {December},

3809 howpublished = {Available from \verb+http://www.haskell.org/+}

3812@misc{perlxs,

3813 title = {Perl {XS} Reference Manual},

3814 author = {Dean Roehrich and {The Perl Porters}},

3815 year = {1996},

3816 howpublished = {\verb+http://www.perldoc.com/perl5.6/pod/perlxs.html+}

3819@misc{swig,

3820 title = {{SWIG} : An Easy to Use Tool for Integrating Scripting Languages with {C} and {C++}},

3821 author = {David M. Beazley},

3822 year = {1996},

3823 howpublished = {\verb+http://www.swig.org/papers/Tcl96/tcl96.html+}

3826@inproceedings{types-prog,

3827 title = {Type Systems for Programming Languages},

3828 booktitle = {Handbook of Theoretical Computer Science},

3829 author = {John C. Mitchell},

3830 pages = {365--458},

3831 year = {1990},

3832 crossref = {htcs}

3835@book{htcs,

3836 title = {Handbook of Theoretical Computer Science},

3837 editor = {J. van Leeuwen},

3838 publisher = {Elsevier Science},

3839 year = {1990}

3842@misc{r5rs,

3843 title = {Revised$^5$ Report on the Algorithmic Language Scheme},

3844 author = {Richard Kelsey and William Clinger and Jonathan Rees},

3845 year = {1998},

3846 month = {February},

3847 howpublished = {Available from \verb+http://www.schemers.org/+}

3850@misc{gmail-outage,

3851 title = {Update on today's {Gmail} Outage},

3852 author = {{Official Gmail Blog}},

3853 howpublished = {\url{http://gmailblog.blogspot.com/2009/02/update-on-todays-gmail-outage.html}},

3854 note = {Retrieved 26th February 2009},

3855 year = 2009