Solving a text layout problem with Dynamic Programming

Secure Counting of members of a subset without revealing their identities

Provably perfect random shuffling and its pure functional implementations

Pure-functional transformations of cyclic graphs and the Credit Card Transform

Radix-2 Fast Fourier Transform: generating optimal code

Practical Lambda-calculators, which implement a normal-order evaluation as a bottom-up parsing

Accumulating tree traversals, a better tree fold, and XML parsing

The probability of randomly chosen integers being relatively prime

Representing knowledge about knowledge

Total stream processors and their applications to all infinite streams

Flattening a (cyclic) list by a lazy virus

Recursively enumerating binary arithmetic relations, from addition to logarithm -- as conjunctions and disjunctions -- in Prolog and Kanren

Provably correct and practical intersection testing of two segments of a circle or two georectangles

On parent pointers in SXML trees

Polymorphic stanamically balanced AVL trees

Selecting a random node from a tree in one pass: from proof to code

Zipper: the context of a traversal

Polymorphic variants as negation of open records: solving the expression problem

Annotating trees post factum
 

XML and Scheme: parsing, querying, authoring, transforming

Functional Style in C++: Closures, Late Binding, and Lambda Abstractions

Purely-functional Object-Oriented System in Scheme

Makefile as a functional language program

Object-Oriented programming is a harmful methodology

KANREN: a declarative logic programming system embedded in Scheme

Declarative Logic Programming in Hansei

Type-level equality, disequality and introspection

Implementing Explicit and Finding Implicit Sharing in Embedded DSLs
 

Typed tagless-final interpretations: Lecture notes

Scheme in Perl, or Perl as Scheme

C pointers as closures

Keyword arguments in Haskell, Scheme macros, ...

Eliminating Array Bound Checking through Non-dependent types and proving it

Symbolic differentiation of compiled numeric functions

Representing existential data types with isomorphic simple types

Unusual polymorphism

Universally polymorphic lists and a polymorphic FOLD in ANSI C without casts
 

Lambda: the ultimate syntax-semantics interface

Many faces of the fixed-point combinator

Type Arithmetic, type-level higher-order for-loops, with applications to safe pointer arithmetic and time-indexed computations

How fundamental is information?

Lexical extensions via macros, and the meaning of identifiers

Applicative syntax-rules: macros that compose better

(Delimited) dynamic binding

Interpreting types as abstract values: a brief course on Hindley-Milner type inference

Recursion from Iteration, an exercise in program derivation
 

Backtracking, indeterministic, state, etc. Monads

UNIX pipes as IO monads. Monadic i/o and UNIX shell programming

Sendmail as a Turing machine

P-numerals: arithmetically more convenient and efficient lambda-numerals

Inverse typechecking and theorem proving in intuitionistic and classical logics

Purely Functional Lazy Non-deterministic Programming

Constructive Law of Excluded Middle
 

Zipper-based file server/OS

Streams, Iteratees and Enumerators: Incremental multi-level input processing

A network file system over HTTP: remote access and modification of files and files A USENIX'99 Freenix track paper

The Web as a computer itself

Persistent delimited continuations for CGI programming with nested transactions

Typed Staged Future: Semi-implicit batched remote code execution as staging
 

Opening of extended file names
including bidirectional and TCP pipes

Kernel of a simple OS in C++

Distributing Data Using TLT30G, Dr. Dobb's Journal, #289, September 1998, pp.34-40, 92-93.

Speaking HTTP: A File-Uploader Tool,
USENIX ;login: -- vol. 25, No. 2 -- April 2000, pp. 6-14.

Delimited continuations in operating systems
 

Flight through/around clouds (a.k.a. Venus)

Grayscale Image Processing

Image Compression Papers