Tarmo Uustalu's recent papers and reports
- T. Altenkirch, J. Chapman, T. Uustalu. Monads need not be
endofunctors.
In C.-H. L. Ong, ed., Proc. of 13th Int. Conf. on
Foundations of Software Science and Computation Structures, FoSSaCS
2010 (Paphos, March 2010), v. 6014 of Lect. Notes in Comput. Sci.,
Springer, to appear.- .pdf, 241K (© Springer)
- K. Nakata, T. Uustalu. A Hoare logic for the coinductive
trace-based big-step semantics of While.
In A. D. Gordon, ed.,
Proc. of 19th Europ. Symp. on Programming, ESOP 2010 (Paphos,
March 2010), v. 6012 of Lect. Notes in Comput. Sci., Springer, to
appear.- .pdf, 229 (© Springer)
- K. Nakata, T. Uustalu. Trace-based coinductive operational
semantics for While: big-step and small-step, relational and
functional styles.
In S. Berghofer, T. Nipkow, C. Urban, M. Wenzel,
eds., Proc. of 22nd Int. Conf. on Theorem Proving in Higher-Order
Logics, TPHOLs 2009 (Munich, Aug. 2009), v. 5674 of
Lect. Notes in Comput. Sci., pp. 375-390. Springer, 2009. - .pdf, 245K (© Springer)
- B. Fischer, A. Saabas, T. Uustalu. Program repair as sound
optimization of broken programs.
In Proc. of 3rd IEEE/IFIP
Int. Symp. on Theoretical Aspects of Software Engineering, TASE 2009
(Tianjin, July 2009), pp. 165-173. IEEE CS Press, 2009. - .pdf, 147K (© IEEE)
- L. Pinto, T. Uustalu. Proof search and counter-model construction
for bi-intuitionistic propositional logic with labelled sequents.
In
M. Giese, A. Waaler, eds., Proc. of 18th Int. Conf. on Automated
Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009
(Oslo, July 2009), v. 5607 of Lect. Notes in
Artif. Intell., pp. 295-309. Springer, 2009. - .pdf, 292K (©
Springer)
- M. J. Frade, A. Saabas, T. Uustalu. Bidirectional data-flow
analyses, type-systematically.
In Proc. of 2009 ACM SIGPLAN
Wksh. on Partial Evaluation and Semantics-Based Program Manipulation,
PEPM 2009 (Savannah, GA, Jan. 2009), pp. 141-149. ACM Press,
2009. - .pdf, 520K (© ACM)
- T. Uustalu, V. Vene. The recursion scheme from the cofree
recursive comonad.
In V. Capretta, C. McBride, eds., Proc. of 2nd
Wksh. on Mathematically Structured Functional Programming, MSFP 2008
(Reykjavík, July 2008), Electron. Notes in
Theor. Comput. Sci., Elsevier, to appear.
- V. Capretta, T. Uustalu, V. Vene. Corecursive algebras: a study
of general corecursion.
In M. Oliveira, J. Woodcock, eds.,
Revised Selected Papers from 12th Brazilian Symp. on Formal
Methods, SBMF 2009 (Gramado, RS, Aug. 2009), v. 5902 of
Lect. Notes in Comput. Sci., pp. 84-100. Springer, 2009. - .pdf, 296K (© Springer)
- A. Saabas, T. Uustalu. Proof optimization for partial redundancy
elimination.
J. of Logic and Algebr. Program., v. 78, n. 7,
pp. 620-643, 2009. - .pdf, 462K
(accepted authors manuscript, © Elsevier Science) //
Conf. version in Proc. of 2008 ACM SIGPLAN Wksh. on Partial
Evaluation and Semantics-Based Program Manipulation, PEPM 2008 (San
Francisco, CA, Jan 2008), pp. 91-101. ACM Press, 2008. - .pdf, 408K (© ACM)
- T. Uustalu, V. Vene. Comonadic notions of computation.
In
J. Adámek, C. Kupke, eds., Proc. of 9th Int. Wksh. on Coalgebraic
Methods in Computer Science, CMCS 2008 (Budapest, Apr. 2008),
v. 203, n. 5 of Electron. Notes in Theor. Comput. Sci.,
pp. 263-284. Elsevier, 2008.- .pdf, 282K
(accepted authors manuscript, © Elsevier Science)
- I. Hasuo, B. Jacobs, T. Uustalu. Categorical views on
computations on trees.
In L. Arge, C. Cachin, T. Jurdzinski,
A. Tarlecki, eds., Proc. of 34th Int. Coll. on Automata, Languages
and Programming, ICALP 2007 (Wroclaw, July 2007), v. 4596
of
Lect. Notes in Comput. Sci., pp. 619-630. Springer,
2007. - .pdf, 505K (© Springer)
- A. Saabas, T. Uustalu. Program and proof optimizations with type
systems.
J. of Logic and Algebraic Programming, v. 77, n. 1-2,
pp. 131-154, 2008. - .pdf, 316K
(accepted authors manuscript, © Elsevier Science)
- M. J. Frade, A. Saabas, T. Uustalu. Foundational certification of
data-flow analyses.
In Proc. of 1st IEEE and IFIP Int. Symp on
Theor. Aspects of Software Engineering, TASE 2007 (Shanghai, June
2007), pp. 107-116. IEEE CS Press, 2007. - .pdf, 280K (© IEEE)
- A. Saabas, T. Uustalu. Type systems for optimizing stack-based
code.
In M. Huisman, F. Spoto, eds., Proc. of 2nd Wksh. on Bytecode
Semantics, Verification, Analysis and Transformation, Bytecode 2007
(Braga, March 2007), v. 190, n. 1 of Electron. Notes in
Theor. Comput. Sci., pp. 103-119. Elsevier, 2007. - .pdf, 304K (accepted authors manuscript, ©
Elsevier Science)
- 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.
Manuscript. - .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, pp. 145-162. Intellect, 2007. - .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
data-flow analyses for imperative
languages.
Theor. Comput. Sci., v. 364, n. 3, pp. 292-310,
2006. - .pdf, 260K (accepted authors
manuscript, © 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.
Theor. Comput. Sci.,
v. 373, n. 3, pp. 273-302, 2007. - .pdf,
325K (accepted authors manuscript, © Elsevier Science) //
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 (accepted authors
manuscript, © Elsevier Science)
- T. Uustalu, V. Vene. The essence of dataflow programming.
In
Z. Horváth, ed., Revised Selected Lectures from 1st Central
European Functional Programming School, CEFP 2005 (Budapest, July
2005), v. 4164
of Lect. Notes in Comput. Sci., pp. 135-167. Springer,
2006. - .pdf, 497K (© Springer)
//
Short conf. version in K. Yi, ed., Proc. of 3rd Asian Symp. on
Programming Languages and Systems, APLAS 2005 (Tsukuba,
Nov. 2005), v. 3780
of Lect. Notes in Comput. Sci., pp. 2-18. Springer,
2005. - .pdf, 363K (©
Springer)
- T. Uustalu, V. Vene. Signals and comonads.
J. of Univ.
Comput. Sci., v. 11, n. 7, pp. 1310-1326, 2005. - .pdf, 135K (© 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,
2004. - .pdf, 255K (©
Springer)
- V. Capretta, T. Uustalu, V. Vene. Recursive coalgebras from
comonads.
Inform. and Comput., v. 204, n. 4, pp. 437-468,
2006. - .pdf, 447K (accepted authors manuscript, © 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. - .pdf, 257K (accepted authors manuscript,
© 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, 2004. - .pdf,
219K (© Springer)
- N. Ghani, T. Uustalu, M. Hamana. Explicit substitutions and
higher-order syntax.
Higher-Order and Symb. Comput., v. 19,
n. 2-3, pp. 263-282, 2006. - .pdf,
330K (© Springer) //
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. - .pdf, 173K (© 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. - .pdf, 255K (accepted authors manuscript, © 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. - .pdf, 305K
- 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. - .pdf, 450K (accepted authors manuscript, ©
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,
2003. - .pdf, 227K (©
Springer)
- 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, 2003. - .pdf,
228K (© Springer)
- 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. - .pdf, 111K
- T. Uustalu, V. Vene, A. Pardo. Recursion schemes from
comonads.
Nordic J. of Computing, v. 8, n. 3, pp. 366-390, 2001. -
.pdf, 318K (© 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. - .pdf, 237K
- 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. - .pdf, 155K (©
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. - .pdf,
296K (accepted authors manuscript, © 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. - .pdf, 255K
Tarmo Uustalu
Last update 30 January 2010