Töökindlate Arvutisüsteemide Uurimise Keskus

Matemaatilised alused ja programmeerimiskeelte tehnoloogia

Kompetents:

struktuurne tõestusteooria, algebraline ja kategoorne loogika, mittestandardsed loogikad, ordinaalanalüüs, algebraline kombinatoorika, funktsionaalprogrammeerimine, programmikeelte semantika, programmianalüüs, sh. tüübipõhised analüüsid, turvalisus programmeerimiskeeltes

Uurimisrühma põhikoosseis:

Tarmo Uustalu, KübI van.-tead. / TTÜ arvutitead. inst. dots. (kuni aug. 2004), prof. (al. sept. 2004) (uurimisrühma juht)
-- tel. 620 4250, epost tarmo (at) cs . ioc . ee
~~Adam Eppendahl, KübI erak. van.-tead. (okt. 2004-juuni 2005)~~
Peeter Laud, TÜ arvutitead. inst. van.-tead./ CybAS van.-tead.
Härmel Nestra, TÜ arvutitead. inst. teadur
~~Jaanus Pöial, TÜ arvutitead. inst. dotsent (kuni aug. 2004)~~
~~Olha Shkaravska, KübI erak. van.-tead. (sept. 2005-aug. 2006)~~
Olga Sokratova, TÜ arvutitead. inst. van.-tead. (tööleping peat.)
Hellis Tamm, KübI erak. van.-tead. (al. sept. 2005)
~~Mati Tombak, TÜ arvutitead. inst. prof. (kuni aug. 2007)~~
Sergei Tupailo, KübI van.-tead. (kuni veebr. 2004 järeldoktorantuuris Leedsi Ülikoolis, okt. 2004-märts 2005 külalisdotsent Ohio Osariigi Ülikoolis, okt. 2007-juuni 2008 külalisdotsent Stanfordi Ülikoolis)
Varmo Vene, TÜ arvutitead. inst. dots. (kuni okt. 2007; peat. sept. 2003-aug. 2005), erak. van.-tead. (sept. 2003-aug. 2005), professor (al. nov. 2007) / KübI van.-tead.
-- tel. 737 5429, epost varmo (at) cs . ut . ee

Doktorandid:

Jevgeni Kabanov, TÜ doktorant (al. sügis 2006)
~~Härmel Nestra, TÜ doktorant (sügis 1998-kevad 2004, kaitsnud)~~
~~Reimo Palm~~
Ahti Peder, TÜ doktorant (al. sügis 2001)
Ando Saabas, TTÜ doktorant (al. sügis 2004)
~~Tiina Zingel, TÜ doktorant (al. sügis 1996)~~
Andres Toom, TTÜ doktorant (al. sügis 2007)
Vesal Vojdani, TÜ doktorant (al. sügis 2005)

Publikatsioone 2003:

A. Abel, R. Matthes, T. Uustalu. 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 Comput. Sci., pp. 54-69. Springer, Berlin, 2003. article at SpringerLink
N. Ghani, T. Uustalu. Coproducts of ideal monads (extended abstract). In Z. Ésik, I. Walukiewicz, eds., Proc. of 5th Int. Wksh. on Fixed Points in Computer Science, FICS'03 (Warsaw, Apr. 2003), pp. 32-36. Warsaw Univ., 2003.
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, MERλIN'03 (Uppsala, Aug. 2003), 7 pp. ACM Press, 2003. doi: 10.1145/976571.976580
A. Kelarev, O. Sokratova. On congruences of automata defined by directed graphs. Theor. Comput. Sci., v. 301, n. 1-3, pp. 31-43, 2003. doi: 10.1016/S0304-3975(02)00544-3
P. Laud. Handling encryption in an analysis for secure information flow. In P. Degano, ed., Proc. of 12th Europ. Symp. on Programming, ESOP 2003 (Warsaw, Apr. 2003), v. 2618 of Lect. Notes in Comput. Sci., pp. 159-173. Springer, Berlin, 2003. article at SpringerLink
P. Laud, R. Corin. Sound computational interpretation of formal encryption with composed keys. In Pre-Proc. of 6th Int. Conf. on Information Security and Cryptology, ICISC 2003 (Seoul, Nov. 2003). 2003.
R. Matthes, T. Uustalu. Substitution in non-wellfounded syntax with variable binding. 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., 15 pp., Elsevier, 2003. doi: 10.1016/S1571-0661(04)80639-X
J. Pöial. Program analysis for stack based languages. In Proc. of 19th EuroForth Conference (Ross-on-Wye, Oct. 2003), pp. 9-13. 2003.
J. Pöial. Implementation of directed multigraphs in Java. In Proc. of 2nd Int. Conf. on Principles and Practice of Programming in Java, PPPJ 2003 (Kilkenny City, June 2003), v. 42 of ACM Int. Conf. Proc. Series, p. 163. Comput. Sci. Press, 2003. article at ACM DL
H. Seidl, V. Vene, M. Müller-Olm. Global invariants for analysing multi-threaded applications. Proc. of Estonian Acad. of Sci., Phys., Math., v. 52, n. 4, pp. 413-436, 2003.
M. Tombak. Logical method in combinatorial counting. In Proc. of Int. Conf. on Advances on Internet, Processing, Systems and Interdisciplinary Research, IPSI 2003 (Sveti Stefan, Oct. 2003), 4 pp. 2003.
S. Tupailo. Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe. Ann. of Pure and Appl. Logic, v. 120, n. 1-3, pp. 165-196, 2003. doi: 10.1016/S0168-0072(02)00065-9
S. Tupailo. Epsilon-substitution method for Δ₁¹-CR: a constructive termination proof. Logic J. of the IGPL, v. 11, n. 3, pp. 367-377, 2003. doi: 10.1093/jigpal/11.3.367
S. Tupailo. On non-wellfounded constructive set theory: construction of non-wellfounded sets in explicit mathematics. In G. Mints, R. Muskens, eds., Games, Logic, and Constructive Sets, v. 161 of CSLI Lect. Notes, pp. 109-125. CSLI Publications, 2003.
T. Uustalu. Generalizing substitution. Theor. Inform. and Appl., v. 37, n. 4, pp. 315-336, 2003. doi: 10.1051/ita:2003022
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 Comput. Sci., pp. 299-315. Springer, Berlin, 2003. article at SpringerLink
T. Uustalu, V. Vene. An alternative characterization of complete iterativeness (extended abstract). In Z. Ésik, I. Walukiewicz, eds., Proc. of 5th Int. Wksh. on Fixed Points in Computer Science, FICS'03 (Warsaw, Apr. 2003), pp. 81-83. Warsaw Univ., 2003.

Publikatsioone 2004:

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. article at SpringerLink
G. Barthe, E. Giménez, M. J. Frade, 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
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 Electron. Notes in Theor. Comput. Sci., pp. 43-61. Elsevier, 2004. doi: 10.1016/j.entcs.2004.02.034
N. Ghani, T. Uustalu. Coproducts of ideal monads. Theor. Inform. and Appl., v. 38, n. 4, pp. 321-342, 2004. doi: 10.1051/ita:2004016
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. article at SpringerLink
N. Ghani, T. Uustalu, V. Vene. Generalizing the augment combinator. In H.-W. Loidl, ed., Proc. of 5th Symp. on Trends in Functional Programming, TFP '04 (München, Nov. 2004), pp. 65-76. Ludwig-Maximilians-Univ. München, 2004.
P. Laud, R. Corin. Sound computational interpretation of formal encryption with composed keys. In J. I. Lim, D. H. Lee, eds., Revised Papers from 6th Int. Conf. on Information Security and Cryptology, ICISC 2003 (Seoul, Nov. 2003), v. 2971 of Lect. Notes in Comput. Sci., pp. 55-66. Springer, 2004. article at SpringerLink
P. Laud. Symmetric encryption in automatic analyses for confidentiality against active adversaries. In Proc. of 2004 IEEE Symp. on Security and Privacy, S&P 2004 (Berkeley, CA, May 2004), pp. 71-85. IEEE CS Press, 2004. doi: 10.1109/secpri.2004.1301316
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
F. Otto, O. Sokratova. Reduction relations for monoid semirings. J. of Symb. Comput., v. 37, n. 3, pp. 343-376, 2004. doi: 10.1016/j.jsc.2003.07.002
S. Tupailo. On the intuitionistic strength of monotone inductive definitions. J. of Symb. Logic, v. 69, n. 3, pp. 790-798, 2004.

Publikatsioone 2005:

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
G. Barthe, T. Rezk, A. Saabas. Proof obligations preserving compilation. In T. Dimitrakos, F. Martinelli, P. Ryan, S. Schneider, eds., Proc. of 3rd Int. Wksh. on Formal Aspects in Security and Trust, FAST '05 (Newcastle upon Tyne, July 2005), Techn. report IIT TR-13/2005, pp. 109-124. Ist. di Informatica e Telematica, Consiglio Nazionale delle Ricerche, 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), pp. 294-305. ACM Press, 2005. doi: 10.1145/1086365.1086403
N. Ghani, P. Johann, T. Uustalu, V. Vene. Monadic augment and generalised short cut fusion. ACM SIGPLAN Notices, v. 40, n. 9, pp. 294-305, 2005. doi: 10.1145/1090189.1086403
A. Kelarev, M. Miller, O. Sokratova. Languages recognized by two-sided automata of graphs. Proc. of Estonian Acad. of Sci.: Phys., Math., v. 54, n. 1, pp. 46-54, 2005.
P. Laud. Secrecy types for a simulatable cryptographic library. In Proc. of 12th ACM Conf. on Computer and Communications Security, CCS 2005 (Alexandria, VA, Nov. 2005), pp. 26-35. ACM Press, 2005. doi: 10.1145/1102120.1102126
P. Laud, T. Uustalu, V. Vene. Type systems equivalent to dataflow analyses for imperative languages. 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.
P. Laud, V. Vene. A type system for computationally secure information flow. In M. Liskiewicz, R. Reischuk, eds., Proc. of 15th Int. Symp. on Fundamentals of Computation Theory, FCT 2005 (Lübeck, Aug. 2005), v. 3623 of Lect. Notes in Comput. Sci., pp. 365-377. Springer, 2005. doi: 10.1007/11537311_32
H. Nestra. Transfinite corecursion. Nordic J. of Computing, v. 12, n. 2, pp. 133-156, 2005.
H. Nestra. Transfinite semantics in program slicing. In V. Vene, M. Meriste, eds., Proc. of 9th Symp. on Programming Languages and Software Tools, SPLST 2005 (Tartu, Aug. 2005), pp. 126-140. Univ. of Tartu, 2005.
H. Nestra. Transfinite semantics in program slicing. Proc. of Estonian Acad. of Sci., Engineering, v. 11, n. 4, pp. 313-328, 2005.
O. Shkaravska. Amortized heap-space analysis for first-order functional programs. In M. van Eekelen, ed., Proc. of 6th Symp. on Trends in Functional Programming, TFP '05 (Tallinn, Sept. 2005), pp. 281-296. Inst. of Cybern., 2005.
O. Shkaravska. Types with semantics: soundness proof assistant. In A. Momigliano, R. Pollack, eds., Proc. of 3rd ACM SIGPLAN Wksh. on Mechanized Reasoning about Languages with Variable Binding, MERλIN '05 (Tallinn, Sept. 2005), pp. 50-57. ACM Press, 2005. doi: 10.1145/1088454.1088461
T. Uustalu, V. Vene. Comonadic functional attribute evaluation. 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.
T. Uustalu, V. Vene. Signals and comonads. 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.
T. Uustalu, V. Vene. Signals and comonads. J. of Univ. Comput. Sci., v. 11, n. 7, pp. 1310-1326, 2005. article at publisher's website
T. Uustalu, V. Vene. The essence of dataflow programming (short 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
V. Vene, T. Uustalu, eds. Revised Lectures from 5th Int. School on Advanced Functional Programming, AFP 2004 (Tartu, Aug. 2004), v. 3622 of Lect. Notes in Comput. Sci., x+357 pp. Springer, 2005. doi: 10.1007/11546382

Publikatsioone 2006:

M. Backes, P. Laud. A mechanized, cryptographically sound type inference checker. In V. Cortier, S. Kremer, eds., Abstracts of 2nd Wksh. on Formal and Computational Cryptography, FCC 2006 (Venice, July 2006), 6 pp. INRIA, 2006.
M. Backes, P. Laud. Computationally sound secrecy proofs by mechanized flow analysis. In Proc. of 13th ACM Conf. on Computer and Communications Security, CCS 2006 (Alexandria, VA, Oct./Nov. 2006), pp. 370-379. ACM Press, 2006. doi: 10.1145/1180405.1180450
G. Barthe, T. Rezk, A. Saabas. Proof obligations preserving compilation. In T. Dimitrakos, F. Martinelli, P. Y. A. Ryan, S. Schneider, eds., Revised Selected Papers from 3rd Int. Wksh. on Formal Aspects in Security and Trust, FAST 2005 (Newcastle upon Tyne, July 2005), v. 3866 of Lect. Notes in Comput. Sci., pp. 112-126. Springer, 2006. doi: 10.1007/11679219_9
V. Capretta, T. Uustalu, V. Vene. Recursive coalgebras from comonads. Inform. and Comput., v. 204, n. 4, pp. 437-468, 2006. doi: 10.1016/j.ic.2005.08.005
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.
N. Ghani, T. Uustalu, M. Hamana. Explicit substitutions and higher-order syntax. Higher-Order and Symbolic Comput., v. 19, n. 2-3, pp. 263-282, 2006. doi: 10.1007/s10990-006-8748-4
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.
S. Gilmore, O. Shkaravska. Estimating the cost of native method calls for resource-bounded functional programming languages. In N. Thomas, ed., Proc. of 2nd Int. Wksh. on Practical Applications of Stochastic Modelling, PASM '05 (Newcastle upon Tyne, July 2005), v. 151, n. 3 of Electron. Notes in Theor. Comput. Sci.. Elsevier, 2006. doi: 10.1016/j.entcs.2006.03.010
M. Hamana, N. Ghani, T. Uustalu, V. Vene. Representing cyclic structures as nested datatypes. In A. Takana, ed., Proc. of 23th Conf. of Japan Society for Software Science and Technology, JSSST 06 (Tokyo, Sept. 2006), 8 pp. Univ. of Tokyo, 2006.
M. Johnson, V. Vene, eds., Proc. of 11th Int. Conf. on Algebraic Methodology and Software Technology, AMAST 2006 (Kuressaare, July 2006), v. 4019 of Lect. Notes in Comput. Sci., xi+389 pp. Springer, 2006. doi: 10.1007/11784180
J. Kabanov, V. Vene. Recursion schemes for dynamic programming. In T. Uustalu, ed., Proc. of 8th Int. Conf. on Mathematics of Program Construction, MPC 2006 (Kuressaare, July 2006), v. 4014 of Lect. Notes in Comput. Sci., pp. 235-252. Springer, 2006. doi: 10.1007/11783596_15
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
C. McBride, T. Uustalu, eds. Proc. of Wksh. on Mathematically Structured Functional Programming, MSFP 2006 (Kuressaare, July 2006), Electron. Wkshs. in Computing. British Comput. Soc., 2006. volume at publisher's website
O. Mürk, J. Kabanov. Aranea: web framework construction and integration kit. In Proc. of 4th Int. Conf. on Principles and Practice of Programming in Java, PPPJ 2006 (Mannheim, Aug./Sept. 2006), v. 178 of ACM Int. Conf. Proc. Series, pp. 163-172. ACM Press, 2006. doi: 10.1145/1168054.1168077
H. Nestra. Fractional semantics. In M. Johnson, V. Vene, eds., Proc. of 11th Int. Conf. on Algebraic Methodology and Software Technology, AMAST 2006 (Kuressaare, July 2006), v. 4019 of Lect. Notes in Comput. Sci., pp. 278-292. Springer, 2006. doi: 10.1007/11784180_22
J. Peetre, J. Penjam, eds. Semigroups and Automata: Selecta Uno Kaljulaid (1941-1999), xxiv+472 pp. IOS Press, 2006. book at IOS Press BooksOnline
J. Pöial. Typing tools for typeless stack languages. In Proc. of 22nd EuroForth Conf. (Cambridge, Sept. 2006), pp. 40-46. 2006.
M. Rathjen, S. Tupailo. Characterizing the interpretation of set theory in Martin-Löf type theory. Ann. of Pure and Appl. Logic, v. 141, n. 3, pp. 442-471, 2006. doi: 10.1016/j.apal.2005.12.008
A. Saabas, T. Uustalu. A compositional natural semantics and Hoare logic for low-level languages. In P. D. Mosses, I. Ulidowski, eds., Proc. of 2nd Wksh. on Structured Operational Semantics, SOS 2005 (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
A. Saabas, T. Uustalu. Compositional type systems for stack-based low-level languages. 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. article at ACM DL
H. Tamm, M. Nykänen, E. Ukkonen. Size reduction of multitape automata. In J. Farré, I. Litovsky, S. Schmitz, eds., Revised Selected Papers from 10th Int. Conf. on Implementation and Application of Automata, CIAA 2005 (Sophia Antipolis, June 2005), v. 3845 of Lect. Notes in Comput. Sci., pp. 307-318. Springer, 2006. doi: 10.1007/11605157_26
H. Tamm, M. Nykänen, E. Ukkonen. On size reduction techniques for multitape automata. Theor. Comput. Sci., v. 363, n. 2, pp. 234-246, 2006. doi: 10.1016/j.tcs.2006.07.027
T. Uustalu, ed. Proc. of 8th Int. Conf. on Mathematics of Program Construction, MPC 2006 (Kuressaare, July 2006), v. 4014 of Lect. Notes in Comput. Sci., x+455 pp. Springer, 2006. doi: 10.1007/11783596
T. Uustalu, V. Vene. The essence of dataflow programming (full version). 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

Publikatsioone 2007:

M. J. Frade, A. Saabas, T. Uustalu. Foundational certification of data-flow analyses. In Proc. of 1st Joint IEEE/IFIP 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
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
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.
P. Laud. On the computational soundness of cryptographically masked flows. In Proc. of 35th Ann. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2008 (San Francisco, CA, Jan. 2008), pp. 337-348. ACM Press, 2008. doi: 10.1145/1328438.1328479
P. Laud. On the computational soundness of cryptographically masked flows. ACM SIGPLAN Notices, v. 43, n. 1, pp. 337-348, 2008. doi: 10.1145/1328897.1328479
C. McBride, T. Uustalu, guest eds. J. of Funct. Program. (Selected Papers from Wksh. on Mathematically Structured Functional Programming, MSFP 2006, Kuressaare, July 2006), to appear.
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
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
A. Saabas, T. Uustalu. Program and proof optimizations with type systems. J. of Logic and Algebraic Program., to appear.
A. Saabas, T. Uustalu. Proof optimization for partial redundancy elimination. 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
H. Tamm. On transition minimality of bideterministic automata. In T. Harju, J. Karhumäki, A. Lepistö, eds., Proc. of 11th Int. Conf. on Developments in Language Theory, DLT 2007 (Turku, July 2007), v. 4588 of Lect. Notes of Comput. Sci., pp. 411-421. Springer, 2007. doi: 10.1007/978-3-540-73208-2_38
H. Tamm. On transition minimality of bideterministic automata. Int. J. of Found. of Comput. Sci., to appear.
M. Tombak. Keerukusteooria. 114 lk. TÜ, 2007.
A. Toom, T. Näks, M. Pantel, M. Gandriau, I. Wati. GeneAuto: an automatic code generator for a safe subset of SimuLink/StateFlow and Scicos. In Proc. of 4th Europ. Conf. on Embedded Real-Time Software, ERTS 2008 (Toulouse, Jan./Feb 2008), to appear.
S. Tupailo. Monotone inductive definitions and consistency of New Foundations. In C. Dimitracopoulos, L. Newelski, D. Normann, eds., Proc. of Logic Coll. 2005 (Athens, July/Aug. 2005), v. 28 of Lect. Notes in Logic, pp. ?-?. Cambridge Univ. Press, 2007.
S. Tupailo. Fixpoints of models construction. Logique et Analyse (Nouvelle Série), v. 50, n. 197, pp. 63-78, 2007.
T. Uustalu, guest ed. Sci. of Comput. Program. (Selected Papers from 8th Int. Conf. on Mathematics of Program Construction, MPC 2006, Kuressaare, July 2006), to appear.
T. Uustalu, V. Vene. Comonadic functional attribute evaluation. In M. van Eekelen, ed., Trends in Functional Programming 6, pp. 145-162. Intellect, 2007.
V. Vojdani, V. Vene. Goblint: path-sensitive data race analysis. In Z. Horváth, L. Kozma, V. Zsók, eds., Proc. of 10th Symp. on Programming Languages and Software Tools, SPLST 2007 (Dobogókö, June 2007), pp. 130-141. Eötvös Loránd Univ., 2007.

Doktorikaitsmised 2004:

H. Tamm, On minimality and size reduction of one-tape and multitape finite automata, Helsingi Ülikool, juhendaja E. Ukkonen, oponent B. W. Watson (Techn. Univ. Eindhoven), 10.12.2004

Doktorikaitsmised 2006:

H. Nestra, Iteratively defined transfinite trace semantics and program slicing with respect to them, Tartu Ülikool, juhendaja V. Vene, oponendid H. Seidl (Techn. Univ. München), T. Uustalu (KübI), 13.10.2006. handle: 10062/1109

Viimane uuendus 31.1.2008