Tarmo Uustalu's research papers
- S.-y. Katsumata, E. Rivas, T. Uustalu. Interaction laws of monads
and comonads.
Manuscript, submitted.
- H. Maarand, T. Uustalu. Reordering derivatives of trace closures
of regular languages.
arXiv preprint 1908.03551, 2019. article in arXiv //
Conf. version in W. Fokkink, R. van Glabbeek,
eds., Proc. of 30th Int. Conf. on Concurrency Theory, CONCUR 2019
(Amsterdam, Aug. 2019), v. 140 of Leibniz. Int. Proc. in
Inf., article 40. Dagstuhl Publishing, 2019.
doi:
10.4230/lipics.concur.2019.40 (open access) (© the
authors) - errata
- D. Ahman, T. Uustalu. Decomposing comonad morphisms.
In M. Roggenbach, A. Sokolova, eds., Proc.
of 8th Conf. on Algebra and Coalgebra in Computer Science, CALCO 2019
(London, June 2019), v. 139 of Leibniz Int. Proc. in Inf.,
article 14. Dagstuhl Publishing, 2019.
doi:
10.4230/lipics.calco.2019.14 (open access) (© the
authors)
- J. Espírito Santo, L. Pinto, T. Uustalu. Modal embeddings and
calling paradigms.
In H. Geuvers, ed., Proc. of 4th Int. Conf.
on Formal Structures for Computation and Deduction, FSCD 2019 (Dortmund,
June 2019), v. 131 of Leibniz Int. Proc. in Inf.,
article 18. Dagstuhl Publishing, 2019. doi:
10.4230/lipics.fscd.2019.18
(open access) (© the authors)
- T. Uustalu, N. Veltri, N. Zeilberger. The sequent calculus of
skew monoidal categories.
In C. Casadio, P. J. Scott, eds., [Joachim
Lambek Memorial Volume], Outstanding Contributions to Logic,
Springer, to appear. //
Conf. version in S. Staton, ed., Proc. of
34th Conf. on Mathematical Foundations of Programming Semantics, MFPS
XXXIV (Halifax, NS, June 2018), v. 341 of Electron. Notes in
Theor. Comput. Sci., pp. 345-370. Elsevier,
2018. doi:
10.1016/j.entcs.2018.11.017 (open access) (© the authors)
- H. Maarand, T. Uustalu. Certified normalization of
generalized traces.
Innov. in Softw. and Syst. Engin., v.
15, n. 3-4, pp. 253-265, 2019. doi:
10.1007/s11334-019-00347-1 (© Springer) //
Conf. version titled Certified Foata
normalization for generalized traces in A. Dutle, C. Muńoz, A.
Narkawicz, eds., Proc. of 10th NASA Formal Methods Symp.,
NFM 2018 (Newport News, VA, Apr. 2018), v. 10811 of Lect.
Notes in Comput. Sci., pp. 299-314. Springer, 2018. doi:
10.1007/978-3-319-77935-5_21 (© Springer)
- T. Uustalu, N. Veltri. Partiality and container monads.
In B.-Y. E. Chang, ed., Proc. of 15th
Asian Symp. on Programming Languages and Systems, APLAS 2017 (Suzhou,
Nov. 2017), v. 10695 of Lect. Notes in Comput. Sci.,
pp. 406-425. Springer,
2017. doi:
10.1007/978-3-319-71237-6_20 (© Springer)
- T. Uustalu. Container combinatorics: monads and lax
monoidal functors.
In M. R. Mousavi, J. Sgall, eds., Proc. of
2nd IFIP WG 1.8 Int. Conf. on Topics in Theoretical Computer Science,
TTCS 2017 (Tehran, Sept. 2017), v. 10608 of Lect. Notes in
Comput. Sci., pp. 91-105. Springer, 2017. doi:
10.1007/978-3-319-68953-1_8 (© IFIP)
- H. Maarand, T. Uustalu. Generating representative executions
(extended abstract).
In V. T. Vasconcelos, P. Haller, eds.,
Proc. of 10th Wksh. on Programming Language Approaches to
Concurrency and Communication-Centric Software, PLACES 2017
(Uppsala, Apr. 2017), v. 246 of Electron. Proc. in
Theor. Comput. Sci., pp. 39-48. Open Publishing Assoc.,
2017. doi:
10.4204/eptcs.246.8 (open access)
- D. Ahman, T. Uustalu. Taking updates seriously.
In R. Eramo, M. Johnson, eds., Proc. of
6th Int. Wksh. on Bidirectional Transformations, BX 2017
(Uppsala, Apr. 2017), v. 1827 of CEUR Wksh. Proc.,
pp. 59-73. RWTH Aachen, 2017. article on publisher's
website (open access)
- T. Uustalu, N. Veltri. The delay monad and restriction
categories.
In D. V. Hung, D. Kapur, eds., Proc. of
14th Int. Coll. on Theoretical Aspects of Computing, ICTAC 2017
(Hanoi, Oct. 2017), v. 10580 of Lect. Notes in
Comput. Sci., pp. 32-50. Springer,
2017. doi:
10.1007/978-3-319-67729-3_3 (© Springer)
- M. Gaboardi, S.-y. Katsumata, D. Orchard, F. Breuvart,
T. Uustalu. Combining effects and coeffects via grading.
In Proc. of 21st ACM SIGPLAN Int. Conf. on
Functional Programming, ICFP '16 (Nara, Sept. 2016) (= ACM
SIGPLAN Notices, v. 51, n. 9), pp. 476-489. ACM Press, 2016. doi:
10.1145/2951913.2951939 (© the authors) - free pdf via ACM
Author-Izer
- T. Uustalu, N. Veltri. Finiteness and rational
sequences, constructively.
J. of Funct. Program., v. 27, article
e13, 2017. doi:
10.1017/s0956796817000041 (© Cambridge University
Press) -
pdf
- D. Ahman, T. Uustalu. Directed containers as categories.
In R. Atkey, N. Krishnaswami, eds.,
Proc. of 6th Wksh. on Mathematically Structured Functional
Programming, MSFP 2016 (Eindhoven, April 2016), v. 207 of
Electron. Proc. in Theor. Comput. Sci., pp. 89-98. Open
Publishing Assoc.,
2016. doi:
10.4204/eptcs.207.5 (open access)
-
errata
- D. Firsov, T. Uustalu, N. Veltri. Variations on
Noetherianness.
In R. Atkey, N. Krishnaswami, eds.,
Proc. of 6th Wksh. on Mathematically Structured Functional
Programming, MSFP 2016 (Eindhoven, April 2016), v. 207 of
Electron. Proc. in Theor. Comput. Sci., pp. 76-88. Open
Publishing Assoc.,
2016. doi:
10.4204/eptcs.207.4 (open access)
- S.-y. Katsumata, T. Sato, T. Uustalu. Codensity lifting of monads
and its dual.
Log. Methods in Comput. Sci., v. 14, n.
4, article 6, 2018. doi:
10.23638/lmcs-14(4:6)2018 (open access) (© the authors)
- L. Pinto, T. Uustalu. A proof theoretic-study of
bi-intuitionistic propositional sequent calculus.
J. of Log. and Comput., v. 28, n. 1, pp.
165-202, 2018. doi:
10.1093/logcom/exx044 (© the authors)
- V. Capretta, T. Uustalu. A coalgebraic view of bar recursion and
bar induction.
In B. Jacobs, C. Löding, eds., Proc. of
19th Int. Conf. on Foundations of Software Science and Computation
Structures, FoSSaCS 2016 (Eindhoven, April 2016), v. 9634 of
Lect. Notes in Comput. Sci., pp. 91-106. Springer,
2016. doi:
10.1007/978-3-662-49630-5_6 (© Springer)
- pdf
- T. Uustalu. A divertimento on MonadPlus and nondeterminism.
J. of Log. and Algebraic Methods in
Program., v. 85, n. 5, part 2, pp. 1086-1094,
2016. doi:
10.1016/j.jlamp.2016.06.004 (© Elsevier Science)
- pdf (accepted
author manuscript)
- J. Chapman, T. Uustalu, N. Veltri. Quotienting the delay monad by
weak bisimilarity.
Math. Struct. in Comput. Sci.,
v. 29, n. 1, pp. 67-92, 2019.
doi:
10.1017/s0960129517000184 (© Cambridge University
Press) //
Conf. version in M. Leucker, C. Rueda,
F. D. Valencia, eds., Proc. of 12th Int. Coll. on Theoretical
Aspects of Computing, ICTAC 2015 (Cali, Oct. 2015), v. 9399
of Lect. Notes in Comput. Sci., pp. 110-125. Springer,
2015. doi:
10.1007/978-3-319-25150-9_8 (© Springer)
- pdf
- D. Firsov, T. Uustalu. Dependently typed programming with finite
sets.
In Proc. of 11th ACM SIGPLAN Wksh. on
Generic Programming, WGP '15 (Vancouver, BC, Aug. 2015),
pp. 33-44. ACM Press,
2015. doi:
10.1145/2808098.2808102 (© the authors)
- free pdf via ACM
Author-Izer
- T. Uustalu. Stateful runners for effectful computations.
In D. Ghica, ed., Proc. of 31st Conf. on
Mathematical Foundations of Programming Semantics, MFPS XXXI
(Nijmegen, June 2015), v. 319 of
Electron. Notes in Theor. Comput. Sci., pp. 403-421,
2015. doi:
10.1016/j.entcs.2015.12.024 (open access) (©
Elsevier Science)
- D. Firsov, T. Uustalu. Certified normalization of context-free
grammars.
In Proc. of 2015 ACM Conf. on Certified
Programs and Proofs, CPP '15 (Mumbai, Jan. 2015),
pp. 167-174. ACM Press,
2015. doi:
10.1145/2676724.2693177 (© the authors)
- free pdf via ACM
Author-Izer
- D. Ahman, T. Uustalu. Coalgebraic update lenses.
In B. Jacobs, A. Silva, S. Staton, eds.,
Proc. of 30th Conf. on Mathematical Foundations of Programming
Semantics, MFPS XXX (Ithaca, NY, June 2014), v. 308 of
Electron. Notes in Theor. Comput. Sci., pp. 25-48. Elsevier,
2014. doi:
10.1016/j.entcs.2014.10.003 (open access) (© Elsevier
Science)
- T. Uustalu. Coherence for skew-monoidal categories.
In N. Krishnaswami, P. Levy, eds.,
Proc. of 5th Wksh. on Mathematically Structured Functional
Programming, MSFP 2014 (Grenoble, Apr. 2014), v. 153 of
Electron. Proc. in Theor. Comput. Sci., pp. 68-77. Open
Publishing Assoc.,
2014. doi:
10.4204/eptcs.153.5 (open access)
-
Agda code
- D. Ahman, T. Uustalu. Update monads: cointerpreting directed
containers.
In R. Matthes, A. Schubert, eds., Proc. of
19th Conf. on Types for Proofs and Programs, TYPES 2013 (Toulouse,
Apr. 2013), v. 26 of Leibniz Int. Proc. in Inform,
pp. 1-23. Dagstuhl Publishing,
2014. doi:
10.4230/lipics.types.2013.1 (open access) (© the authors)
- J. Chapman, T. Uustalu, N. Veltri. Formalizing restriction
categories.
J. of Formaliz. Reason., v. 10, n. 1,
pp. 1-36,
2017. doi:
10.6092/issn.1972-5787/6237 (open access) (© the authors)
- D. Firsov, T. Uustalu. Certified CYK parsing of context-free
languages.
J. of Log. and Algebraic Meth. in
Program., v. 83, n. 5-6, pp. 459-468,
2014. doi:
10.1016/j.jlamp.2014.09.002 (© Elsevier Science)
- pdf (accepted author
manuscript)
- D. Firsov, T. Uustalu. Certified parsing of regular languages.
In G. Gonthier, M. Norrish, eds., Proc. of
3rd Int. Conf. on Certified Programs and Proofs, CPP 2013
(Melbourne, Dec. 2013), v. 8307 of Lect. Notes in
Comput. Sci., pp. 98-113. Springer,
2013. doi:
10.1007/978-3-319-03545-1_7 (© Springer)
- pdf
- T. Uustalu. Coinductive big-step semantics for concurrency.
In W. Vanderbauwhede, N. Yoshida, eds.,
Proc. of 6th Wksh. on Programming Language Approaches to
Concurrency and Communication-Centric Software, PLACES 2013
(Rome, March 2013), v. 137 of Electron. Proc. in
Theor. Comput. Sci., pp. 63-78. Open Publishing Assoc.,
2013. doi:
10.4204/eptcs.137.6 (open access)
-
Haskell code
- D. Ahman, T. Uustalu. Distributive laws of directed containers.
Progress in Informatics, v. 10,
pp. 3-18,
2013. doi:
10.2201/niipi.2013.10.2 (open access)
-
Haskell code //
Extended abstract in L. Schröder,
D. Pattinson, eds., Short Contributions of 11th Int. Wksh. on
Coalgebraic Methods in Comput. Sci., CMCS '12 (Tallinn,
March/April 2012), pp. 1-3. Inst. of Cybernetics, 2012. -
pdf
- T. Uustalu. Structured general corecursion and coinductive graphs
(extended abstract).
In Z. Ésik, D. Miller, eds., Proc. of 8th
Wksh. on Fixed Points in Computer Science, FICS 2012 (Tallinn,
March 2012), v. 77 of Electron. Proc. in
Theor. Comput. Sci., pp. 55-61. Open Publishing Assoc.,
2012. doi:
10.4204/eptcs.77.8 (open access)
- T. Uustalu. Explicit binds: effortless efficiency with and without
trees.
In T. Schrijvers, P. Thiemann, eds.,
Proc. of 11th Int. Symp. on Functional and Logic Programming,
FLOPS 2012 (Kobe, May 2012), v. 7294 of Lect. Notes in
Comput. Sci., pp. 317-331. Springer,
2012. doi:
10.1007/978-3-642-29822-6_25 (© Springer)
- pdf, Haskell code
- D. Ahman, J. Chapman, T. Uustalu. When is a container a
comonad?
Log. Methods in Comput. Sci., v. 10,
n. 3, article 14,
2014. doi:
10.2168/lmcs-10(3:14)2014 (open access) (© the authors)
//
Conf. version in L. Birkedal,
ed., Proc. of 15th Int. Conf. on Foundations of Software Science
and Computation Structures, FoSSaCS 2012 (Tallinn, March 2012),
v. 7213 of Lect. Notes in Comput. Sci., pp. 74-88. Springer,
2012. doi:
10.1007/978-3-642-28729-9_5 (© Springer)
- pdf,
project page,
incl. Agda code
- K. Nakata, T. Uustalu, M. Bezem. A proof pearl with the fan
theorem and bar induction: walking through infinite trees with mixed
induction and coinduction.
In H. Yang, ed., Proc. of 9th Asian
Symp. on Programming Languages and Systems, APLAS 2011 (Kenting,
Dec. 2011), v. 7078 of Lect. Notes in Comput. Sci.,
pp. 353-368. Springer,
2011. doi:
10.1007/978-3-642-25318-8_26 (© Springer)
- pdf
- M. Bezem, K. Nakata, T. Uustalu. On streams that are finitely
red.
Log. Methods in Comput. Sci., v. 8,
n. 4, article 4,
2012. doi:
10.2168/lmcs-8(4:4)2012 (open access) (© the authors)
- S. Capobianco, T. Uustalu. A categorical outlook on cellular
automata.
In J. Kari, ed., Proc. of 2nd Symp. on
Cellular Automata, JAC 2010 (Turku, Dec. 2010), v. 13 of TUCS
Lecture Notes, pp. 88-99. Turku Centre for Computer Science,
2010. - pdf
- L. Pinto, T. Uustalu. Relating sequent calculi for
bi-intuitionistic propositional logic.
In S. van Bakel, S. Berardi, U. Berger, eds.,
Proc. of 3rd Wksh. on Classical Logic and Computation CL&C
2010 (Brno, Aug. 2010), v. 47 of Electron. Proc. in
Theor. Comput. Sci., pp. 57-72. Open Publishing Assoc.,
2011. doi:
10.4204/eptcs.47.7 (open access)
- T. Uustalu. A note on strong dinaturality, initial algebras and
uniform parameterized fixpoint operators (extended abstract).
In L. Santocanale, ed., Proc. of 7th
Wksh. on Fixed Points in Computer Science, FICS 2010 (Brno,
Aug. 2010), pp. 77-82. Masarykova Univ., 2010. - pdf
- K. Nakata, T. Uustalu. Resumptions, weak bisimilarity and big-step
semantics for While with interactive I/O: an exercise in mixed
induction-coinduction.
In L. Aceto, P. Sobocinski, eds., Proc. of
7th Wksh. on Structural Operational Semantics, SOS 2010 (Paris,
Aug. 2010), v. 32 of Electron. Proc. in
Theor. Comput. Sci., pp. 57-75. Open Publishing Assoc.,
2010. doi:
10.4204/eptcs.32.5 (open access)
- T. Uustalu. Strong relative monads (extended abstract).
In B. Jacobs, M. Niqui, J. Rutten, A. Silva,
eds., Short Contributions of 10th Int. Wksh. on Coalgebraic
Methods in Comput. Sci., CMCS '10 (Paphos, March 2010),
pp. 23-24. CWI, 2010. - pdf
- T. Altenkirch, J. Chapman, T. Uustalu. Relative monads
formalised.
J. of Formaliz. Reason., v. 7, n. 1,
pp. 1-43,
2014. doi:
10.6092/issn.1972-5787/4389 (open access) (© the authors)
- T. Altenkirch, J. Chapman, T. Uustalu. Monads need not be
endofunctors.
Log. Methods in Comput. Sci., v. 11,
n. 1, article 3,
2015. doi:
10.2168/lmcs-11(1:3)2015 (open access) (© the authors)
//
Conf. version in 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., pp. 297-311. Springer,
2010. doi:
10.1007/978-3-642-12032-9_21 (© Springer)
- pdf
- K. Nakata, T. Uustalu. A Hoare logic for the coinductive
trace-based big-step semantics of While.
Log. Methods in Comput. Sci., v. 11,
n. 1, article 1,
2015. doi:
10.2168/lmcs-11(1:1)2015 (open access) (© the authors)
//
Conf. version 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.,
pp. 488-506. Springer,
2010. doi:
10.1007/978-3-642-11957-6_26 (© Springer)
- pdf
- 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. doi:
10.1007/978-3-642-03359-9_26 (© Springer)
- pdf
- B. Fischer, A. Saabas, T. Uustalu. Program repair as sound
optimization of broken programs.
In
Proc. of 3rd IEEE Int. Symp. on Theoretical Aspects of Software
Engineering, TASE 2009 (Tianjin, July 2009), pp. 165-173. IEEE
CS Press, 2009. doi:
10.1109/tase.2009.61 (© IEEE)
- pdf
- 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. doi:
10.1007/978-3-642-02716-1_22 (© Springer)
- pdf
- 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. doi:
10.1145/1480945.1480965 (© ACM)
- free pdf via ACM
Author-Izer
- 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), v. 229, n. 5 of
Electron. Notes in Theor. Comput. Sci.,
pp. 135-157. Elsevier,
2011. doi:
10.1016/j.entcs.2011.02.020 (open access) (© Elsevier
Science)
- 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.
doi:
10.1007/978-3-642-10452-7_7 (© Springer)
- pdf
- A. Saabas, T. Uustalu. Proof optimization for partial redundancy
elimination.
J. of Log. and Algebraic Program.,
v. 78, n. 7, pp. 620-643,
2009. doi:
10.1016/j.jlap.2009.05.002 (open access) (© 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. doi:
10.1145/1328408.1328422 (© ACM)
- free pdf via ACM
Author-Izer (via ACM
Author-Izer)
- 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. doi:
10.1016/j.entcs.2008.05.029 (open access) (© Elsevier
Science)
- B. Jacobs, T. Uustalu. Semantics of grammars and attributes
via initiality.
In E. Barendsen, V. Capretta, H. Geuvers, M.
Niqui, eds., Reflections on Type theory, Lambda-Calculus, and the
Mind: Essays Dedicated to Henk Barendregt on the Occasion of His
60th Birthday, pp. 181-196. Radboud Univ. Nijmegen, 2007. article
on publisher's webpage (open access)
- 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. doi:
10.1007/978-3-540-73420-8_54 (© Springer)
- pdf
- A. Saabas, T. Uustalu. Program and proof optimizations with type
systems.
J. of Log. and Algebraic Program.,
v. 77, n. 1-2, pp. 131-154,
2008. doi:
10.1016/j.jlap.2008.05.007 (open access) (© 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. doi:
10.1109/tase.2007.27 (© IEEE) -
pdf
- 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. doi:
10.1016/j.entcs.2007.02.063 (open access) (© 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
- A. Saabas, T. Uustalu. Compositional type systems for stack-based
low-level languages.
Manuscript. - pdf //
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 Inf. Technol.,
pp. 27-39. Australian Comput. Soc., 2006.
article in
ACM DL (© Australian Comput. Soc.)
- pdf
- T. Uustalu, V. Vene. Comonadic functional attribute
evaluation.
In M. van Eekelen, ed.,
Trends in Functional Programming 6, pp. 145-162. Intellect,
2007.
book in Google Books
- pdf //
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. doi:
10.1016/j.tcs.2006.08.013 (open access) (© 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. doi:
10.1016/j.tcs.2006.12.020 (open access) (© 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. doi:
10.1016/j.entcs.2005.09.031 (open access) (© 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. doi:
10.1007/11894100_5 (© Springer)
- pdf //
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. doi:
10.1007/11575467_2 (© Springer)
- pdf
- T. Uustalu, V. Vene. Signals and comonads.
J. of Univ.
Comput. Sci., v. 11, n. 7, pp. 1310-1326, 2005.
doi:
10.3217/jucs-011-07-1311 (open access) (© J.UCS)
//
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. doi:
10.1145/1086365.1086403 (© ACM)
- free pdf via ACM
Author-Izer
- 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. book
in Google Books - pdf
- 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. doi:
10.1007/978-3-540-30477-7_22 (© Springer)
- pdf
- N. Ghani, T. Uustalu. Monad combinators, non-determinism and
probabilistic choice (extended abstract).
Manuscript, distributed at CMCIM 2004
(Copenhagen, Aug. 2004) - pdf
- V. Capretta, T. Uustalu, V. Vene. Recursive coalgebras from
comonads.
Inf. and Comput., v. 204, n. 4,
pp. 437-468,
2006. doi:
10.1016/j.ic.2005.08.005 (open access) (© 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. doi:
10.1016/j.entcs.2004.02.034 (open access) (© 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. doi:
10.1007/978-3-540-24754-8_19 (© Springer)
- pdf
- N. Ghani, T. Uustalu, M. Hamana. Explicit substitutions and
higher-order syntax.
High.-Order and Symb. Comput., v. 19,
n. 2-3, pp. 263-282,
2006. doi:
10.1007/s10990-006-8748-4 (© Springer)
- pdf //
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. doi:
10.1145/976571.976580 (© ACM)
- free pdf via ACM
Author-Izer
- N. Ghani, T. Uustalu. Coproducts of ideal
monads.
Theor. Inf. and Appl., v. 38, n. 4,
pp. 321-342, 2004. doi:
10.1051/ita:2004016 (© EDP Science)
- free
pdf from NUMDAM //
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.
- T. Uustalu, V. Vene. An alternative characterization of
complete iterativeness (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. 81-83. Warsaw Univ., 2003. -
pdf
- R. Matthes, T. Uustalu. Substitution in non-wellfounded syntax
with variable binding.
Theor. Comput. Sci., v. 327, n. 1-2,
pp. 155-174,
2004. doi:
10.1016/j.tcs.2004.07.025 (open access) (© 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. doi:
10.1016/s1571-0661(04)80639-x (open access) (© Elsevier
Science)
- 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. doi:
10.1016/j.tcs.2004.10.017 (open access) (© 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. doi:
10.1007/3-540-36576-1_4 (© Springer)
- pdf
- 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. doi:
10.1007/3-540-39185-1_17 (© Springer)
- pdf
- T. Uustalu. Generalizing substitution.
Theor. Inf. and Appl., v. 37, n. 4,
pp. 315-336, 2003. doi:
10.1051/ita:2003022 (© EDP Sciences)
- free
pdf from NUMDAM //
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. doi:
10.1145/509799.503043 (© ACM) -
free pdf via ACM
Author-Izer
- 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. - pdf
- 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. book in Google
Books - pdf
- T. Uustalu, V. Vene, A. Pardo. Recursion schemes from
comonads.
Nordic J. of Computing, v. 8, n. 3,
pp. 366-390, 2001. (© Publ. Assoc. Nordic J. of Computing)
- pdf
- 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. doi:
10.1017/s0960129503004122 (© Cambridge Univ. Press)
- pdf
- T. Uustalu, V. Vene. Coding recursion ŕ 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., Univ.
Utrecht, 2000.
- pdf
- T. Uustalu, V. Vene. Mendler-style inductive types,
categorically.
Nordic J. of Computing, v. 6, n. 3,
pp. 343-361, 1999. (© Publ. Assoc. Nordic J. of Computing)
- pdf
- T. Uustalu. Multi-(co)iteration, categorically.
In J. Penjam, ed., Proc. of 6th
Fenno-Ugric Symp. on Software Technology, FUSST '99 (Sagadi,
Aug. 1999), Report CS 104/99, pp. 259-267. Inst. of Cybernetics,
1999. - pdf
- T. Uustalu, V. Vene. Primitive (co)recursion and course-of-value
(co)iteration, categorically.
Informatica, v. 10, n. 1, pp. 5-26,
1999. doi:
10.3233/inf-1999-10102, article
on publisher's website (open access) (© Inst. of Math. and
Inf.)
- 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. issue in Google
Books (© Estonian Academy Publishers)
- pdf
- 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. doi:
10.1016/s0304-3975(00)00355-8 (open access) (© Elsevier
Science)
- T. Uustalu. Natural deduction for intuitionistic least and
greatest fixedpoint logics, with an application to program
construction.
PhD thesis, Diss. TRITA-IT AVH 98:03, Dept. of Teleinformatics, Royal
Inst. of Technol., Stockholm, 1998.
- 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
- T. Uustalu. Aspects of structural synthesis of programs.
Lic thesis, Research Report TRITA-IT R 95:09,
Dept. of Teleinformatics, Royal Inst. of Technol., Stockholm,
1995.
- B. Mayoh, E. Tyugu, T. Uustalu. Constraint satisfaction and
constraint programming: a brief lead-in.
In B. Mayoh, E. Tyugu, J. Penjam, eds.,
Proc. of NATO ASI on Constraint Programming (Pärnu, Aug. 1993),
v. 131 of NATO ASI Series F, pp. 1-16. Springer,
1994. doi:
10.1007/978-3-642-85983-0_1 (© Springer)
- E. Tyugu, T. Uustalu. Higher-order functional constraint
networks.
In B. Mayoh, E. Tyugu, J. Penjam, eds.,
Proc. of NATO ASI on Constraint Programming (Pärnu, Aug. 1993),
v. 131 of NATO ASI Series F, pp. 116-139. Springer,
1994. doi:
10.1007/978-3-642-85983-0_5 (© Springer)
- T. Uustalu. Combining object-oriented and logic paradigms: a modal
logic programming approach.
In O. Lehrmann Madsen, ed., Proc. of 6th
Europ. Conf. on Object-Oriented Programming, ECOOP '92 (Utrect,
June/July 1992), v. 615 of Lect. Notes in Comput. Sci.,
pp. 98-113. Springer,
1992. doi:
10.1007/bfb0053032 (© Springer)
- pdf
- T. Uustalu. Combination of object-oriented and logic paradigms.
MSc thesis, Tallinn Techn. Univ., 1992.
(Written at Norwegian Inst. of Technol., Trondheim, 1991.) -
pdf
- T. Uustalu, P. Lorents. On some classes of hereditarily
r.e. sets.
Proc. of Estonian Acad. Sci.: Phys.,
Math., v. 39, n. 2, pp. 108-112, 1990. (In Russian.)
(© Estonian Academy Publishers)
- pdf
- T. Uustalu, M. Pentus. Sequent systems of modal calculi.
Preprint. Inst. of Cybernetics, 1989. (In
Russian.) (© Estonian Academy Publishers)
- pdf
- T. Uustalu. On recursive functionals of higher types.
In Abstracts of Conf. on Theoretical and
Applied Questions in Mathematics (Tartu, Sept. 1985), v. 1,
pp. 188-190. Univ. of Tartu, 1985. (In Russian.) - pdf
Tarmo Uustalu
Last update 25 November 2019