Prototype implementation of a language Push, accompanying our recently submitted paper. The prototype is implemented and prepared by Ta-Chung Tsai.
While studying XML stream processing, we noticed that programmers need concurrency to save space, especially in a lazy language. We propose the idea of pushing datatypes — when a pushing closure is demanded, all expressions referring to it are evaluated concurrently to weak head normal forms. The closure is no more alive and may thus be garbage collected.
[GZipped Tarball]
Research
λ calculus Agda Bidirectional Updating Burrows-Wheeler Transform Concurrency Converse-of-a-Function Theorem Curry-Howard Data Structure Dependent Type Fibonacci GADT Greedy Theorem Haskell HaXML List Homomorphism Logic Logic Programming Program Derivation Program Inversion Quantum Programming Quine Regular Expression Segment Problems Termination Thinning Theorem Types XML Streaming-
Recent Comments
- 先寬度標記 on Theory and applications of inverting functions as folds.
- Liang-Ting Chen on Proof Irrelevance, Extensional Equality, and the Excluded Middle
- Shin on Proof Irrelevance, Extensional Equality, and the Excluded Middle
- speleologic on Proof Irrelevance, Extensional Equality, and the Excluded Middle
- Dan Doel on No Inverses for Injective but Non-Surjective Functions?
AoPA — Algebra of Programming in Agda