!
133p. http://folli.loria.fr/cds/1999/library/pdf/barrwells.pdf
61p. http://www.dcs.ed.ac.uk/home/dt/CT/categories.pdf
182p. http://www.cs.utah.edu/plt/publications/pllc.pdf
R5RSの Formal Semantics にある Semantic functions と Auxiliary functions を scheme 自身で実装したもの。半自動生成らしいです。 http://www.appsolutions.com/SchemeDS/
10p.目次。 Introduction Simple Trampolining Interleaved Trampolining Stepping Sequential Composition Breakpoints Engines Dynamic Thread Creation Varying the Granularity of Parallelism with Multiple Trampolining Revisionist History: CPS as …
(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://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/
目次。 $0 Introduction $1 Versions of Epistemic Closure. $2 In favor of closure principle (4). $3 Heavyweight Propositions and Conclusive Reasons. $4 Residual Puzzles.
http://www.missouri.edu/~kvanvigj/papers/Closure%20and%20Contrastive%20Knowledge.pdf http://plato.stanford.edu/entries/logical-constants/
(via logblog) 「形式的である」ということについての歴史。かなりの分量。 http://philosophy.berkeley.edu/macfarlane/diss.html
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…
目次。 Introduction Multiple Return Values Implementation Rewriting values and call-with-values Procedure call interface Register-based return count Stack-based return count Separate multiple-value return point Procedural versions of value…
目次。 Introduction Scheme as an IntermediateRepresentation What is an IR? An Introduction to Scheme Why Scheme? CurrentScheme Implementations Scheme Speed Scheme Architecture Advantageous Scheme Semantics Scoping First-class Procedures Co…
http://www.grappa.univ-lille3.fr/tata/
(via Lambda the Ultimate) http://www.ki.inf.tu-dresden.de/%7Eguglielm/res/pap/PrThFoundLP.pdf
http://uq.net.au/~zzdkeena/Lambda/index.htm
