Tarmo Uustalu's research papers
- T. Uustalu, N. Veltri, N. Zeilberger. Deductive systems and
coherence for skew prounital closed categories.
In C. Sacerdoti
Coen, A. Tiu, eds., Proc. of 15th Int. Wksh. on Logical
Frameworks and Metalanguages: Theory and Practice, LFMTP 2020
(Paris, June 2020), v. 332 of Electron. Proc. in Theor. Comput.
Sci., pp. 35-53. Open Publishing Assoc., 2021.
doi:10.4204/eptcs.332.3
(open access) (© the authors)
- T. Uustalu, N. Voorneveld. Algebraic and coalgebraic perspectives
on interaction laws.
In B. C. d. S. Oliveira, ed., Proc. of 18th
Asian Symp. on Programming Languages and Systems, APLAS 2020 (Fukuoka,
Nov./Dec. 2020), v. 12470 of Lect. Notes in Comput. Sci., pp.
186-205. Springer, 2020. doi:10.1007/978-3-030-64437-6_10
(© Springer) - pdf
- D. McDermott, M. Piróg, T. Uustalu. Degrading lists.
In Proc. of 22nd Int. Symp. on Principles
and Practice of Declarative Programming, PPDP 2020 (Bologna, Sept.
2020), ACM Int. Conf. Proc. Series, article 6, 14 pp. ACM Press,
2020. doi:10.1145/3414080.3414084
(© the authors) - pdf, Haskell code
(exotic list monads)
- T. Uustalu, N. Veltri, N. Zeilberger. Proof theory of partially
normal skew monoidal categories.
In D. I. Spivak, J. Vicary, eds., Proc. of
3rd Applied Category Theory Conf. (Cambridge, MA, July 2020), v. 333
of Electron. Proc. in Theor. Comput. Sci., pp. 230-246. Open
Publishing Assoc., 2021. doi:10.4204/eptcs.333.16
(open access) (© the authors) - video
- T. Uustalu, N. Veltri, N. Zeilberger. Eilenberg-Kelly reloaded.
Electron. Notes in Theor. Comput. Sci.,
v. 352 (P. Johann, ed., Proc. of 36th Conf. on Mathematical Foundations
of Programming Semantics, MFPS XXXVI, Paris, June 2020), pp. 233-256,
2020. doi:10.1016/j.entcs.2020.09.012
(open access) (© the authors) - slides, video
- H. Maarand, T. Uustalu. Operational semantics with semicommutations.
Manuscript, submitted.
- S. Katsumata, E. Rivas, T. Uustalu. Interaction laws of monads
and comonads.
Full version as arXiv eprint 1912.13477, 2019. arXiv:1912.13477
//
Conf. version in Proc. of 35th Ann. ACM/IEEE
Symp. on Logic in Computer Science, LICS 2020 (Saarbrücken, July
2020), pp. 604-618. ACM Press, 2020. doi:10.1145/3373718.3394808
(© the authors) - pdf, slides, video
- H. Maarand, T. Uustalu. Reordering derivatives of trace closures
of regular languages.
Full version as arXiv eprint 1908.03551, 2019. arXiv:1908.03551 //
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) - corrigendum, video from
Estonian-Latvian CS Theory Days in Pärnu
- 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: The Interplay of Mathematics, Logic, and Linguistics,
v. 20 of Outstanding Contributions to Logic, Springer, to appear. (© the authors)
//
Conf. version in Electron. Notes in Theor.
Comput. Sci., v. 341 (S. Staton, ed., Proc. of 34th Conf. on Mathematical
Foundations of Programming Semantics, MFPS XXXIV, Halifax, NS, June
2018), pp. 345-370, 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)
- pdf
- 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) -
pdf
- 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) -
pdf
- 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 at
publisher (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) -
pdf
- M. Gaboardi, S. Katsumata, D. Orchard, F. Breuvart,
T. Uustalu. Combining effects and coeffects via grading.
Reprinted in ACM SIGPLAN Notices, v. 51,
n. 9, pp. 476-489, 2016. doi:10.1145/3022670.2951939 //
In Proc. of 21st ACM SIGPLAN Int. Conf. on
Functional Programming, ICFP '16 (Nara, Sept. 2016), pp. 476-489.
ACM Press, 2016. doi:10.1145/2951913.2951939
(© the authors) - free pdf via ACM
Author-Izer, video
- 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)
-
corrigendum
- 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. 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) -
pdf
- 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
(open access) (© Elsevier Science)
Extended abstract distributed at 4th ACM
SIGPLAN Wksh. on Higher-Order Programming with Effects, HOPE 2015,
Vancouver, BC, Aug. 2015. - video
- 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.
Electron. Notes in Theor. Comput. Sci.,
v. 319 (D. Ghica, ed., Proc. of 31st Conf. on Mathematical
Foundations of Programming Semantics, MFPS XXXI, Nijmegen, June
2015), 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.
Electron. Notes in Theor. Comput. Sci.,
v. 308 (B. Jacobs, A. Silva, S. Staton, eds.,
Proc. of 30th Conf. on Mathematical Foundations of Programming
Semantics, MFPS XXX, Ithaca, NY, June 2014), pp. 25-48, 2014.
doi:10.1016/j.entcs.2014.10.003
(open access) (© Elsevier
Science)
-
errata
- 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)
-
corrigendum
- 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
(open access) (© Elsevier Science)
- 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.
Electron. Notes in Theor. Comput. Sci.,
v. 229, n. 5 (V. Capretta, C. McBride, eds.,
Proc. of 2nd Wksh. on Mathematically Structured Functional
Programming, MSFP 2008, Reykjavík, July 2008), pp. 135-157, 2011.
doi:10.1016/j.entcs.2011.02.020
(open access) (© Elsevier Science)
-
Haskell code
- 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.
Electron. Notes in
Theor. Comput. Sci., v. 203, n. 5 (J. Adámek, C. Kupke, eds.,
Proc. of
9th Int. Wksh. on Coalgebraic Methods in Computer Science, CMCS 2008,
Budapest, Apr. 2008), pp. 263-284, 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
at publisher (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.
Electron. Notes in
Theor. Comput. Sci., v. 190, n. 1 (M. Huisman, F. Spoto, eds.,
Proc. of
2nd Wksh. on Bytecode Semantics, Verification, Analysis and
Transformation, Bytecode 2007, Braga, March 2007), pp. 103-119,
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 Electron. Notes in
Theor. Comput. Sci., v. 156, n. 1 (P. D Mosses, I. Ulidowski, eds.,
Proc. of 2nd Wksh. on Structured Operational Semantics, SOS '05,
Lisbon, July 2005), pp. 151-168, 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.
Reprinted in ACM SIGPLAN Notices, v.
40, n. 9, pp. 294-305, 2005. doi:10.1145/1090189.1086403
//
In Proc. of 10th ACM SIGPLAN Int. Conf. on
Functional Programming, ICFP '05 (Tallinn, Sept. 2005), 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 Electron. Notes in
Theor. Comput. Sci., v. 106 (J. Adámek, S. Milius, eds., Proc. of
7th Int. Wksh. on Coalgebraic Methods in Computer Science,
CMCS '04, Barcelona, March 2004), pp. 43-61, 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, Haskell code //
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 Electron. Notes in
Theor. Comput. Sci., v. 82, n. 1 (H. P. Gumm, ed., Proc. of 6th
Int. Wksh. on Coalgebraic Methods in Computer Science, CMCS '03,
Warsaw, Apr. 2003), pp. 191-205, 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).
Reprinted in ACM SIGPLAN Notices, v. 37,
n. 3, pp. 131-142, 2002. doi:10.1145/509799.503043
//
In Proc. of 2002 ACM SIGPLAN Wksh. on
Partial Evaluation and Semantics-Based Program Manipulation,
PEPM '02 (Portland, OR, Jan. 2002), pp. 131-142. ACM Press,
2002. doi:10.1145/503032.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
at publisher (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) - pdf
- 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) - pdf
- 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 31 January 2021