Tarmo Uustalu's recent papers and reports

• N. Ghani, M. Hamana, T. Uustalu, V. Vene. Representing cyclic structures as nested datatypes. In H. Nilsson, ed., Proc. of 7th Symp. on Trends in Functional Programming, TFP 2006 (Nottingham, Apr. 2006), pp. 173-188. Univ. of Nottingham, 2006. - .pdf, 72K
• A. Saabas, T. Uustalu. Compositional type systems for stack-based low-level languages. Submitted. - .pdf, 402K // Conf. version in B. Jay, J. Gudmundsson, eds., Proc. of 12th Computing, Australasian Theory Symp., CATS 2006 (Hobart, Jan. 2006), v. 51 of Confs. in Research and Practice in Inform. Techn., pp. 27-39. Australian Comput. Soc., 2006. - .pdf, 270K (© Australian Comput. Soc.)
• T. Uustalu, V. Vene. Comonadic functional attribute evaluation. In M. van Eekelen, ed., Trends in Functional Programming 6, Intellect, to appear. - .pdf, 67K // Conf. version in M. van Eekelen, ed., Proc. of 6th Symp. on Trends in Functional Programming, TFP '05 (Tallinn, Sept. 2005), pp. 33-43. Inst. of Cybern., 2005.
• P. Laud, T. Uustalu, V. Vene. Type systems equivalent to dataflow analyses for imperative languages. Theor. Comput. Sci., to appear. - .pdf, 260K (© Elsevier Science) // Conf. version in M. Hofmann, H.-W. Loidl, eds., Proc. of 3rd APPSEM II Wksh., APPSEM '05 (Frauenchiemsee, Sept. 2005), 12 pp. Ludwig-Maximilians-Univ. München, 2005.
• A. Saabas, T. Uustalu. A compositional natural semantics and Hoare logic for low-level languages. Submitted. - .pdf, 320K // Conf. version in P. D Mosses, I. Ulidowski, eds., Proc. of 2nd Wksh. on Structured Operational Semantics, SOS '05 (Lisbon, July 2005), v. 156, n. 1 of Electron. Notes in Theor. Comput. Sci., pp. 151-168. Elsevier, 2006. - .pdf, 269K (© Elsevier Science)
• T. Uustalu, V. Vene. The essence of dataflow programming. In Z. Horváth, ed., Revised Lectures from Central European Functional Programming School, CEFP 2005 (Budapest, July 2005), v. 4164 of Lect. Notes in Comput. Sci., Springer-Verlag, to appear. - .pdf, 255K (© Springer-Verlag) // Short conf. version in K. Yi, ed., Proc. of 3rd Asian Symp. on Programming Languages and Systems, APLAS'05 (Tsukuba, Nov. 2005), v. 3780 of Lect. Notes in Comput. Sci., pp. 2-18. Springer-Verlag, 2005. - .pdf, 363K (© Springer-Verlag)
• T. Uustalu, V. Vene. Signals and comonads. J. of Univ. Comput. Sci., v. 11, n. 7, pp. 1310-1326, 2005. - .pdf, 119K (© J. of Univ. Comput. Sci.) // Conf. version in M. A. Musicante, R. M. F. Lima, eds., Proc. of 9th Brazilian Symp. on Programming Languages, SBLP'05 (Recife, PE, May 2005), pp. 215-228. Univ. de Pernambuco, Recife, 2005.
• N. Ghani, P. Johann, T. Uustalu, V. Vene. Monadic augment and generalised short cut fusion. In Proc. of 10th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP '05 (Tallinn, Sept. 2005) (= ACM SIGPLAN Notices, v. 40, n. 9), pp. 294-305. ACM Press, 2005. - .pdf, 144K (© ACM)
• N. Ghani, T. Uustalu, V. Vene. Generalizing the augment combinator. In H.-W. Loidl, ed., Trends in Functional Programming 5, pp. 65-78. Intellect, 2006. - .pdf, 74K
• 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 2004 (Taipei, Nov. 2004), v. 3302 of Lect. Notes in Comput. Sci., pp. 327-347. Springer-Verlag, 2004. - .pdf, 255K (© Springer-Verlag)
• V. Capretta, T. Uustalu, V. Vene. Recursive coalgebras from comonads. Inform. and Comput., v. 204, n. 4, pp. 437-468, 2006. - (© Elsevier Science) // Conf. version 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 Electron. Notes. in Theor. Comput. Sci., pp. 43-61. Elsevier, 2004. - .ps.gz, 219K (© Elsevier Science)
• T. Altenkirch, T. Uustalu. Normalization by evaluation for λ^→,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 Comput. Sci., pp. 260-275. Springer-Verlag, 2004. - .pdf, 219K (© Springer-Verlag)
• N. Ghani, T. Uustalu, M. Hamana. Explicit substitutions and higher-order syntax. Higher-Order and Symb. Comput., v. 19, n. 2-3, to appear. - .pdf, 330K // Conf. version in F. Honsell, M. Miculan, A. Momigliano, eds., Proc. of 2nd ACM SIGPLAN Wksh. on Mechanized Reasoning about Languages with Variable Binding, MERλIN '03 (Uppsala, Aug. 2003), 7 pp. 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 5th Int. Wksh. on Fixed Points in Computer Science, FICS '03 (Warsaw, Apr. 2003), pp. 32-36. Warsaw Univ., 2003.
• R. Matthes, T. Uustalu. Substitution in non-wellfounded syntax with variable binding. Theor. Comput. 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 Electron. Notes. in Theor. Comput. Sci.. Elsevier, 2003. - .ps.gz, 116K
• A. Abel, R. Matthes, T. Uustalu. Iteration schemes for higher-order and nested datatypes. Theor. Comput. 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 2003 (Warsaw, Apr. 2003), v. 2620 of Lect. Notes in Comput. 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 2002 (Berg en Dal, Apr. 2002), v. 2646 of Lect. Notes in Comput. 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 4th Int. Wksh. on Fixed Points in Computer Science, FICS '02 (Copenhagen, 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) (= ACM 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. Univ. de É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
• 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 Comput. 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, pp. 69-85. Dept. of Comput. Sci., Utrecht Univ., 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 Acad. of Sci.: 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. Theor. Comput. Sci., 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 μ,ν-logic. In M. Haveraaen, O. Owe, eds, Selected Papers from 8th Nordic Wksh. on Programming Theory, NWPT '96 (Oslo, Dec. 1996), Research Report 248, pp. 237-246. Inst. for Informatikk, Univ. i Oslo, 1997. - .ps.gz, 120K