Tarmo Uustalu's recent papers and reports

• N. Ghani, T. Uustalu, V. Vene. Build, augment and destroy, universally. In W.-N. Chin, ed., Proc. of 2nd Asian Symp. on Programming Languages and Systems, APLAS'04 (Taipei, Nov. 2004), v. 3302 of Lect. Notes in Comp. Sci., pp. 327-347. Springer-Verlag, 2004. - .ps.gz, 184K (© Springer-Verlag)

• V. Capretta, T. Uustalu, V. Vene. Recursive coalgebras from comonads. In J. Adámek, S. Milius, eds., Proc. of 7th Int. Wksh. on Coalgebraic Methods in Computer Science, CMCS'04 (Barcelona, March 2004), v. 106 of Electr. Notes. in Theor. Comp. Sci., pp. 43-61. Elsevier, 2004. - .ps.gz, 219K (© Elsevier Science)

• T. Altenkirch, T. Uustalu. Normalization by evaluation for lambda^arrow,2. In Y. Kameyama, P. J. Stuckey, eds., Proc. of 7th Int. Symp. on Functional and Logic Programming, FLOPS 2004 (Nara, Apr. 2004), v. 2998 of Lect. Notes. in Comp. Sci., pp. 260-275. Springer-Verlag, 2004. - .ps.gz, 162K (© Springer-Verlag)

• N. Ghani, T. Uustalu. Explicit substitutions and higher-order syntax. In F. Honsell, M. Miculan, A. Momigliano, eds., Proc. of 2nd ACM SIGPLAN Wksh. on Mechanized Reasoning about Languages with Variable Binding, MERLIN'03 (Uppsala, Aug. 2003) ACM Press, 2003. - .ps.gz, 117K (© ACM)

• N. Ghani, T. Uustalu. Coproducts of ideal monads. Theor. Inform. and Appl., v. 38, n. 4, pp. 321-342, 2004. - .ps.gz, 255K (© EDP Sciences) // Extended abstract in Z. Ésik, I. Walukiewicz, ed., Proc. of Int. Wksh. on Fixed Points in Computer Science, FICS'03 (Warsaw, Apr. 2003), pp. 32-36. Warsaw Univ., 2003.

• T. Uustalu, V. Vene. An alternative characterization of complete iterativeness (extended abstract). In Z. Ésik, I. Walukiewicz, ed., Proc. of Int. Wksh. on Fixed Points in Computer Science, FICS'03 (Warsaw, Apr. 2003), pp. 81-83. Warsaw Univ., 2003.

• R. Matthes, T. Uustalu. Substitution in non-wellfounded syntax with variable binding. Theor. Comp. Sci., v. 327, n. 1-2, pp. 155-174, 2004. - (© Elsevier Science) // Conf. version in H. P. Gumm, ed., Proc. of 6th Int. Wksh. on Coalgebraic Methods in Computer Science, CMCS'03 (Warsaw, Apr. 2003), v. 82, n. 1 of Electr. Notes. in Theor. Comp. Sci.. Elsevier, 2003. - .ps.gz, 116K

• A. Abel, R. Matthes, T. Uustalu. Iteration schemes for higher-order and nested datatypes. Theor. Comp. Sci., v. 333, n. 1-2, pp. 3-66, 2005. - (© Elsevier Science) // Conf. version Generalized iteration and coiteration for higher-order nested datatypes in A. D. Gordon, ed., Proc. of 6th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS'03 (Warsaw, Apr. 2003), v. 2620 of Lect. Notes in Comp. Sci., pp. 54-69. Springer-Verlag, 2003. - .ps.gz, 80K (© Springer-Verlag)

• T. Uustalu. Monad translating inductive and coinductive types. In H. Geuvers, F. Wiedijk, eds., Selected Papers from 2nd Int. Wksh. on Types for Proofs and Programs, TYPES'02 (Berg en Dal, Apr. 2002), v. 2646 of Lect. Notes in Comp. Sci., pp. 299-315. Springer-Verlag, 2003. - .ps.gz, 76K (© Springer-Verlag)

• T. Uustalu. Generalizing substitution. Theor. Inform. and Appl., v. 37, n. 4, pp. 315-336, 2003. - .ps.gz, 222K (© EDP Sciences) // Extended abstract in Z. Ésik, A. Ingólfsdóttir, eds., Prel. Proc. of Wksh. on Fixed Points in Computer Science, FICS'02 (Copenhagen, Denmark, July 2002), BRICS Notes Series NS-02-2, pp. 9-11. Dept. of Computer Science, Univ. of Aarhus, 2002.

• G. Barthe, T. Uustalu. CPS translating inductive and coinductive types (extended abstract). In Proc. of 2002 ACM SIGPLAN Wksh. on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'02 (Portland, OR, Jan. 2002), SIGPLAN Notices, v. 37, n. 3, pp. 131-142. ACM Press, 2002. - .ps.gz, 84K (© ACM)

• T. Uustalu. (Co)monads from inductive and coinductive types. In L M. Pereira, P. Quaresma, eds, Proc of 2001 APPIA-GULP-PRODE Joint Conf. on Declarative Programming, AGP'01 (Évora, Sept. 2001), pp. 47-61, Dept. of Informatics, Univ. of Évora, 2001.

• T. Uustalu, V. Vene. The dual of substitution is redecoration. In K. Hammond, S. Curtis, eds, Trends in Functional Programming 3, pp. 99-110. Intellect, Bristol / Portland, OR, 2002. - .ps.gz, 46K (© Intellect)

• T. Uustalu, V. Vene, A. Pardo. Recursion schemes from comonads. Nordic J. of Computing, v. 8, n. 3, pp. 366-390, 2001. - .ps.gz, 115K (© Publ. Assoc. Nordic J. of Computing)

• G. Barthe, M. J. Frade, E. Giménez, L. Pinto, T. Uustalu. Type-based termination of recursive definitions. Math. Struct. in Comp. Sci., v. 14, n. 1, pp. 97-141, 2004. - .ps.gz, 172K (© Cambridge Univ. Press)

• T. Uustalu, V Vene. Coding recursion a la Mendler (extended abstract). In J. Jeuring, ed, Proc of 2nd Wksh on Generic Programming, WGP'2000 (Ponte de Lima, July 2000), Techn. Report UU-CS-2000-19, Dept. of Comp. Sci., Utrecht Univ., pp 69-85, 2000. - .ps.gz, 94K

• T. Uustalu, V Vene. Mendler-style inductive types, categorically. Nordic J. of Computing, v. 6, n. 3, pp. 343-361, 1999. - .ps.gz, 107K (© Publ. Assoc. Nordic J. of Computing)

• T. Uustalu, V Vene. Primitive (co)recursion and course-of-value (co)iteration, categorically. Informatica, v. 10, n. 1, pp. 5-26, 1999. - .ps.gz., 91K (© Inst. of Math. and Inform.)

• V Vene, T. Uustalu. Functional programming with apomorphisms (corecursion). Proc. of Estonian Academy of Sciences: Phys., Math., v. 47, n. 3, pp. 147-161, 1998. - .ps.gz, 115K (© Estonian Academy Publishers)

• T. Uustalu, V Vene. Least and greatest fixed-points in intuitionistic natural deduction. Theoretical Computer Science, v. 272, n. 1-2, pp. 315-339, 2002. - .ps.gz, 121K, preprint version (© Elsevier Science)

• T. Uustalu, V Vene. A cube of proof systems for the intuitionistic predicate mu-,nu-logic. In M. Haveraaen, O. Owe, eds, Selected Papers from 8th Nordic Wksh. on Programming Theory, NWPT'96 (Oslo, Dec. 1996), Research Report 248, Dept. of Informatics, Univ. of Oslo, pp. 237-246, 1997. - .ps.gz, 120K