118p. http://www.cs.ut.ee/~varmo/papers/thesis.pdf http://www.cs.ut.ee/~varmo/

182p. http://www.cs.utah.edu/plt/publications/pllc.pdf

44p.何故か一つのファイルに同じ内容のものが二つ入っている（ただ、前にある方に一ページの欠落がある）ので、実際には22p。 目次。 Context The Problem A simple example Functors Types as initial fixed points Paramorphisms relationship with catamo…

(via Lambda tha Ultimate) 8p.目次。 Introduction Calculi for shift and reseet The original λξ-calculus Purity as answer type polymorphism Direct-style transforms On to polarized liner logic Conclusion and related work Acknowledgements http…

(via Lambda the Ultimate) 8p.目次。 Introduction Bidirectional Fold Unidirectional Scan Bidirectional Scan Mapping Scans Conclusion http://www.dcs.gla.ac.uk/publications/paperdetails.cfm?id=7063

15p.目次。 Gentzen's natural deducation Charch's lambda calculus Typed lambda calculus The Curry-Howard correspondence Conclusions http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf

http://www.jetcafe.org/~jim/lambda.html

http://web.engr.oregonstate.edu/~erwig/meta/

273p. http://folli.loria.fr/cds/1999/library/pdf/curry-howard.pdf

378p. http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/

http://dst.purevoid.org/

http://www-2.cs.cmu.edu/~rwh/theses/okasaki.pdf

目次。 Introduction The fold operator The universal property of fold Universality as a proof principle The fusion property of fold Universality as a definition principle Increasing the power of fold: generating tuples Primitive recursion U…

目次。 Introduction The data type of lists Catamorphisms Anamorphisms Hylomorphisms Paramorphisms Algebraic data types Functors Recursive types Recursion Schemes Program Calculation Laws Catamorphisms Anamorphisms Hylomorphisms Relating ca…

目次。 Introduction λ-calculus From terms to nets Interaction net reduction From nets to terms Static correctness Directed nets Tree nets The automaton Reading back trees Binding loops λ-nets △≅▲ Dynamic correctness Related and further wor…

http://uq.net.au/~zzdkeena/Lambda/index.htm