Programming languages and systems (PLS)

Key persons

T. Uustalu, V. Vene, S. Capobianco, J. Chapman, K. Nakata, H. Nestra, J. Penjam, H. Tamm

Postdocs

W. Jeltsch

Logic and semantics research group of IoC

Publications 2008

W. Dosch, A. Stümpel, T. Tamme. Streaming dyadic boolean operations. In Proc. of 5th Int. Conf. on Information Technology: New Generations, ITNG 2008 (Las Vegas, NV, Apr. 2008), pp. 88-96. IEEE CS Press, 2008. doi: 10.1109/itng.2008.210 (WOS: 000255578800015)
J. Kabanov, R. Raudjärv. Embedded typesafe domain specific languages for Java. In Proc. of 6th Int. Conf. on Principles and Practice of Programming in Java, PPPJ 2008 (Modena, Sept. 2008), v. 347 of ACM Int. Conf. Proc. Series, pp. 189-197. ACM Press, 2008. doi: 10.1145/1411732.1411758
A. Saabas, T. Uustalu. Program and proof optimizations with type systems. J. of Logic and Algebraic Program., v. 77, n. 1-2, pp. 131-154, 2008. doi: 10.1016/j.jlap.2008.05.007 (WOS: 000259762900007)
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 (WOS: 000267583600010)
H. Tamm. On transition minimality of bideterministic automata. Int. J. of Found. of Comput. Sci., v. 19, n. 3, pp. 677-690, 2008. doi: 10.1142/s0129054108005887 (WOS: 000256383100011)
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 J.-C. Laprie, ed., Proc. of 4th Europ. Conf. on Embedded Real-Time Software, ERTS 2008 (Toulouse, Jan./Feb 2008), 10 pp. SIA, 2008. article at publisher's website
T. Uustalu, J. Vain, J. Ernits, eds., Abstracts of 20th Nordic Wksh. on Programming Theory, NWPT 2008 (Tallinn, Nov. 2008), 106 pp. Inst. of Cybernetics, 2008. volume at workshop website
T. Uustalu, V. Vene. Comonadic notions of computation. In J. Adámek, C. Kupke, eds., Proc. of 9th Int. Wksh. on Coalgebraic Methods in Comput. Sci., CMCS 2008 (Budapest, March 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
M. Veanes, A. Saabas. On bounded reachability of programs with set comprehensions. In I. Cervesato, H. Veith, A. Voronkov, eds., Proc. of 15th Int. Conf. on Logic for Programming, Artif. Intell. and Reasoning, LPAR 2008 (Doha, Nov. 2008), v. 5330 of Lect. Notes in Artif. Intell., pp. 305-317. Springer, 2008. doi: 10.1007/978-3-540-89439-1_22 (WOS: 000262502600022)
M. Veanes, A. Saabas. Using satisfiability modulo theories to analyze abstract state machines (abstract). In E. Börger, M. Butler, J. P. Bowen, P. Boca, eds., Proc. of 1st Int. Conf. on Abstract State Machines, B and Z, ABZ 2008 (London, Sept. 2008), v. 5238 of Lect. Notes in Comput. Sci., p. 355. Springer, 2008. doi: 10.1007/978-3-540-87603-8_42 (WOS: 000260118300041)

Publications 2009

T. Altenkirch, J. Chapman. Big-step normalisation. J. of Funct. Program., v. 19, n. 3-4, pp. 311-333, 2009. doi: 10.1017/s0956796809007278 (WOS: 000267240300004)
S. Capobianco. On the induction operation for shift subspaces and cellular automata as presentations of dynamical systems. Inform. and Comput., v. 207, n. 11, pp. 1169-1180, 2009. doi: 10.1016/j.ic.2009.02.006 (WOS: 000271169800006)
S. Capobianco. Some notes on Besicovitch and Weyl distances over higher-dimensional configurations. In P. P. B. de Oliveira, J. Kari, eds., Proc. of 15th Int. Wksh. on Cellular Automata and Discrete Complex Systems, AUTOMATA 2009 (São José dos Campos, SP, Oct. 2009), pp. 300-308. Univ. Presbiteriana Mackenzie, 2009.
V. Capretta, T. Uustalu, V. Vene. Corecursive algebras: a study of general structured corecursion. In M. Oliveira, J. Woodcock, eds., Proc. of 12th Brazilian Symp. on Formal Methods, SBMF 2009 (Gramado, RS, Aug. 2009), pp. 84-100. Univ. Federal do Rio Grande do Sul, 2009.
V. Capretta, T. Uustalu, V. Vene. Corecursive algebras: a study of general structured 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 (WOS: 000276970300007)
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 (WOS: 000272549300021)
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
R. Matthes, T. Uustalu, eds. Proc. of 6th Wksh. on Fixed Points in Computer Science, FICS 2009 (Coimbra, Sept. 2009), 124 pp. Inst. of Cybernetics, 2009. volume at workshop website
C. McBride, T. Uustalu, guest eds. J. of Funct. Program., v. 19, n. 3-4 (Selected Papers from 1st Wksh. on Mathematically Structured Functional Programming, MSFP 2006, Kuressaare, July 2006), pp. 263-488, 2009. doi: 10.1017/s0956796809007242 (WOS: 000267240300001)
K. Nakata, M. Hasegawa. Small-step and big-step semantics for call-by-need. J. of Funct. Program, v. 19, n. 6, pp. 699-722, 2009. doi: 10.1017/s0956796809990219 (WOS: 000272196200004)
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 (WOS: 000272047000026)
H. Nestra. Transfinite semantics in the form of greatest fixpoint. J. of Logic and Algebr. Program., v. 78, n. 7, pp. 574-593, 2009. doi: 10.1016/j.jlap.2009.03.001 (WOS: 000270600300006)
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 (WOS: 000271335100021)
A. Saabas, T. Uustalu. Proof optimization for partial redundancy elimination. J. of Logic and Algebr. Program., v. 78, n. 7, pp. 619-642, 2009. doi: 10.1016/j.jlap.2009.05.002 (WOS: 000270600300008)
H. Seidl, V. Vojdani. Region analysis for race detection. In J. Palsberg, Z. Su, eds., Proc. of 16th Int. Static Analysis Symp., SAS 2009 (Los Angeles, CA, Aug. 2009), v. 5673 of Lect. Notes in Comput. Sci., pp. 171-187. Springer, 2009. doi: 10.1007/978-3-642-03237-0_13 (WOS: 000269952100011)
H. Seidl, V. Vojdani, V. Vene. A smooth combination of linear and Herbrand equalities for polynomial time must-alias analysis. In A. Cavalcanti, D. Dams, eds., Proc. of 2nd World Congress on Formal Methods, FM 2009 (Eindhoven, Nov. 2009), v. 5850 of Lect. Notes in Comput. Sci., pp. 644-659. Springer, 2009. doi: 10.1007/978-3-642-05089-3_41 (WOS: 000279900600041)
T. Uustalu, guest ed. Sci. of Comput. Program., v. 74, n. 8 (Selected Papers from 8th Int. Conf. on Mathematics of Program Construction, MPC 2006, Kuressaare, July 2006), pp. 497-668, 2009. doi: 10.1016/j.scico.2009.02.001 (WOS: 000266671700001)
V. Vojdani, V. Vene. Goblint: path-sensitive data race analysis. Ann. Univ. Sci. Budapestinensis de Rolando Eötvös Nomin., Sectio Computat., v. 30, pp. 141-156, 2009.

Publications 2010

T. Altenkirch, J. Chapman, T. Uustalu. Monads need not be endofunctors. 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 (WOS: 000278827800021)
T. Altenkirch, T. Uustalu, guest eds. Fundam. Inform., v. 102, n. 2 (Special Issue on Dependently Typed Programming), pp. 145-228, 2010. doi: 10.3233/fi-2010-302 (WOS: 000282138500001)
A. Annamaa, A. Breslav, J. Kabanov, V. Vene. An interactive tool for analyzing embedded SQL queries. In K. Ueda, ed., Proc. of 8th Asian Symp. on Programming Languages and Systems, APLAS 2010 (Shanghai, Dec. 2010), v. 6461 of Lect. Notes in Comput. Sci., pp. 131-138. Springer, 2010. doi: 10.1007/978-3-642-17164-2_10 (WOS: 000290881800010)
S. Capobianco. On pattern density and sliding block code behavior for the Besicovich and Weyl pseudo-distances. In J. van Leeuwen, A. Muscholl, D. Peleg, J. Pokorny, B. Rumpe, eds., Proc. of 36th Int. Conf. on Current Trends in Theory and Practice of Computer Science, SOFSEM 2010 (Špindleruv Mlýn, Jan. 2010), v. 5901 of Lect. Notes in Comput. Sci., pp. 259-270. Springer, 2010. doi: 10.1007/978-3-642-11266-9_22 (WOS: 000280086900022)
S. Capobianco, T. Toffoli. Dissipative CA computation without power sources? J. of Cellular Automata, v. 5, n. 3, pp. 169-183, 2010. article at publisher's website (WOS: 000276557000002)
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. volume at DORIA, article at HAL
V. Capretta, J. Chapman, eds. Proc. of 3rd ACM SIGPLAN Wksh. on Mathematically Structured Functional Programming, MSFP 2010 (Baltimore, MD, Sept. 2010), vi+56 pp. ACM Press, 2010. volume at ACM DL
J. Chapman, P.-E. Dagand, C. McBride, P. Morris. The gentle art of levitation. In Proc. of 15th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2010 (Baltimore, MD, Sept. 2010), pp. 3-14. ACM Press, 2010. doi: 10.1145/1863543.1863547 (WOS: 000287113300002)
J. Chapman, P.-E. Dagand, C. McBride, P. Morris. The gentle art of levitation. ACM SIGPLAN Notices, v. 45, n. 9, pp. 3-14, 2010. doi: 10.1145/1932681.1863547 (WOS: 000286594300002)
J. Kreiker, H. Seidl, V. Vojdani. Shape analysis of low-level C with overlapping structures. In G. Barthe, M. Hermenegildo, eds., Proc. of 11th Int. Conf. on Verification, Model Checking and Abstract Interpretation, VMCAI 2010 (Madrid, Jan. 2010), v. 5944 of Lect. Notes in Comput. Sci., pp. 214-230. Springer, 2010. doi: 10.1007/978-3-642-11319-2_17 (WOS: 000278758100016)
K. Nakata. Denotational semantics for lazy initialization of letrec: black holes as exceptions rather than divergence. In L. Santocanale, ed., Proc. of 7th Wksh. on Fixed Points in Computer Science, FICS 2010 (Brno, Aug. 2010), pp. 61-67. Masarykova Univ., 2010. proceedings volume at HAL
K. Nakata, A. Sabelfeld. Securing class initialization. In M. Nishigaki, A. Jøsang, Y. Murayama, S. Marsh, eds., Proc. of 4th IFIP WG 11.11 Int. Conf. on Trust Management, IFIPTM 2010 (Morioka, June 2010), v. 321 of IFIP Advances in Information and Communication Technology, pp. 48-62. Springer, 2010. doi: 10.1007/978-3-642-13446-3_4
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., pp. 488-506. Springer, 2010. doi: 10.1007/978-3-642-11957-6_26 (WOS: 000279369000025)
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. 2010. doi: 10.4204/eptcs.32.5
M. Pettai. Untyped general polymorphic functions. In J. Hage, ed., Preproc. of 22nd Symp. on Implementation and Application of Functional Languages, IFL 2010 (Alphen aan den Rijn, Sept. 2010), 16 pp. Univ. Utrecht, 2010. proceedings volume at publisher's website
H. Tamm. Some minimality results on biresidual and biseparable automata. In A. H. Dediu, H. Fernau, C. Martin-Vide, eds., Proc. of 4th Int. Conf. on Language and Automata Theory and Applications, LATA 2010 (Trier, May 2010), v. 6031 of Lect. Notes in Comput. Sci., pp. 573-584. Springer, 2010. doi: 10.1007/978-3-642-13089-2_48 (WOS: 000279649600048)
A. Toom, N. Izerrouken, T. Näks, M. Pantel, O. Ssi Yan Kai. Towards reliable code generation with an open tool: evolutions of the Gene-Auto toolset. In Proc. of 5th Europ. Conf. on Embedded Real-Time Software and Systems, ERTS² 2010 (Toulouse, May 2010), 10 pp. SIA, 2010. article at conference website
A. Toom, N. Izerrouken, T. Näks, M. Pantel, O. Ssi Yan Kai. Towards reliable code generation with an open tool: evolutions of the Gene-Auto toolset. Ingénieurs de l'Automobile, n. 807, pp. 29-35, 2010.
E. Tyugu. Grigori Mints and computer science. In S. Feferman, W. Sieg, eds., Proofs, Categories and Computations: Essays in Honor of Grigori Mints, v. 13 of Tributes Series, pp. 267-277. College Publications, 2010.
T. Uustalu. A note on strong dinaturality, initial algebras and uniform parameterized fixpoint operators. 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. proceedings volume at HAL
T. Uustalu, J. Vain, guest eds. J. of Log. and Algebr. Program., v. 79, n. 7 (Selected Papers from 20th Nordic Wksh. on Programming Theory, NWPT 2008, Tallinn, Nov. 2008), pp. 435-703, 2010. doi: 10.1016/j.jlap.2010.07.002 (WOS: 000282544000001)

Publications 2011

J. Brzozowski, H. Tamm. Theory of átomata. In G. Mauri, A. Leporati, eds., Proc. of 15th Int. Conf. on Developments in Language Theory, DLT 2011 (Milano, July 2011), v. 6795 of Lect. Notes in Comput. Sci., pp. 105-116. Springer, 2011. doi: 10.1007/978-3-642-22321-1_10
S. Capobianco. Generalized Besicovitch and Weyl spaces: topology, patterns, and sliding block codes. Theor. Comput. Sci., v. 412, n. 30, pp. 3822-3837, 2011. doi: 10.1016/j.tcs.2011.02.020 (WOS: 000292589800004)
S. Capobianco, P. Guillon, J. Kari. Garden-of-Eden-like theorems for amenable groups. In N. Fatés, E. Goles, A. Maass, I. Rapaport, eds., Proc. of 17th Int. Wksh. on Cellular Automata and Discrete Complex Systems, AUTOMATA 2011 (Santiago, Nov. 2011), pp. 233-242. Universidad de Chile, 2011.
S. Capobianco, T. Toffoli. Can anything from Noether's theorem be salvaged for discrete dynamical systems? In C. S. Calude, J. Kari, I. Petre, G. Rozenberg, eds., Proc. of 10th Int. Conf. on Unconventional Computation, UC 2011 (Turku, June 2011), v. 6714 of Lect. Notes in Comput. Sci., pp. 77-88. Springer, 2011. doi: 10.1007/978-3-642-21341-0_13
H. Im, K. Nakata, J. Garrigue, S. Park. A syntactic type system for recursive modules. In Proc. of 2011 ACM Int. Conf. on Object-Oriented Programming, Systems, Languages and Applications, OOPSLA 2011 (Portland, OR, Oct. 2011), pp. 993-1012. ACM Press, 2011. doi: 10.1145/2048066.2048141
H. Im, K. Nakata, J. Garrigue, S. Park. A syntactic type system for recursive modules. ACM SIGPLAN Notices, v. 46, n. 10, pp. 993-1012. doi: 10.1145/2076021.2048141
J. Kabanov. JRebel tool demo. In D. Pichardie, ed., Proc. of 5th Wksh. on Bytecode Semantics, Verification, Analysis and Transformation, BYTECODE 2010 (Paphos, March 2010), v. 264, n. 4 of Electron. Notes in Theor. Comput. Sci., pp. 51-57. Elsevier, 2011. doi: 10.1016/j.entcs.2011.02.005
J. Kabanov, M. Hunger, R. Raudjärv. On designing safe and flexible embedded DSLs with Java 5. Sci. of Comput. Program., v. 76, n. 11, pp. 970-991, 2011. doi: 10.1016/j.scico.2010.04.005 (WOS: 000292671000002)
K. Nakata. Resumption-based big-step and small-step interpreters for While with interactive I/O. In O. Danvy, C.-c. Shan, eds., Proc. of IFIP Working Conf. on Domain-Specific Languages, DSL 2011 (Bordeaux, Sept. 2011), v. 66 of Electron. Proc. in Theor. Comput. Sci., pp. 226-235, 2011. doi: 10.4204/eptcs.66.12
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
H. Nestra. Purely functional global variables. In J. Penjam, ed., Proc. of 12th Symp. on Programming Languages and Software Tools, SPLST 2011 (Tallinn, Oct. 2011), pp. 20-31. Inst. of Cybern., 2011.
A. Peder, H. Nestra, J. Raik, M. Tombak, R. Ubar. Linear algorithms for testing superpositional graphs. In E. Dubrova, ed., Proc. of Reed-Muller Workshop (Tuusula, May 2011), pp. 111-118. Tampere Univ. of Techn., 2011.
A. Peder, H. Nestra, J. Raik, M. Tombak, R. Ubar. Linear algorithms for recognizing and parsing superpositional graphs. Facta Universitatis: Electronics and Energetics, v. 24, n. 3, pp. 325-339, 2011.
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, 2011. doi: 10.4204/eptcs.47.7
M. Schwarz, H. Seidl, V. Vojdani, M. Müller-Olm, P. Lammich. Static analysis of interrupt-driven programs. In Proc. of 38th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, POPL '11 (Austin, TX, Jan. 2011), pp. 93-104. ACM Press, 2011. doi: 10.1145/1926385.1926398 (WOS: 000289656100009)
M. Schwarz, H. Seidl, V. Vojdani, M. Müller-Olm, P. Lammich. Static analysis of interrupt-driven programs. ACM SIGPLAN Notices, v. 46, n. 1, pp. 93-104, 2011. doi: 10.1145/1925844.1926398 (WOS: 000286472700009)
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
H. Yu, Y. Ma, Y. Glouche, J.-P. Talpin, T. Gautier, P. Le Guernic, L. Besnard, A. Toom, O. Laurent. System-level co-simulation of integrated avionics using Polychrony. In Proc. of 26th Ann. ACM Symp. on Applied Computing, SAC '11 (TaiChung, March 2011), pp. 354-359. ACM Press, 2011. doi: 10.1145/1982185.1982263

Publications 2012

D. Ahman, J. Chapman, T. Uustalu. When is a container a comonad? In L. Birkedal, ed., Proc. of 15th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2012 (Tallinn, March 2012), Lect. Notes in Comput. Sci., Springer, to appear.

T. Altenkirch, J. Chapman, T. Uustalu. Monads need not be endofunctors. Logical Methods in Computer Science, to appear.

T. Altenkirch, J. Chapman, T. Uustalu. Relative monads formalized. J. of Formalized Reasoning, to appear.

M. Bezem, K. Nakata, T. Uustalu. On streams that are finitely red. Logical Methods in Computer Science, to appear.

M. Bordin, T. Näks, A. Toom, M. Pantel. Compilation of heterogeneous models: motivations and challenges. In Proc. of 7th Europ. Conf. on Embedded Real-Time Software and Systems, ERTS2 2012 (Toulouse, Feb. 2012), SIA, to appear.

J. Garrigue, K. Nakata. Path resolution for nested recursive modules. Higher-Order and Symbolic Computation, to appear.

R. Matthes, T. Uustalu, guest eds. Theor. Inform. and Appl. (Selected Papers from 6th Wksh. on Fixed Points in Comput. Sci., Coimbra, Sept. 2009), to appear.

T. Uustalu. Structured general corecursion and coinductive graphs. In Z. Ésik, D. Miller, eds., Proc. of 8th Wksh. on Fixed Points in Computer Science, FICS 2012 (Tallinn, March 2012), Electron. Proc. in Theor. Comput. Sci., to appear.

PhD defenses 2008

A. Saabas. Logics for Low-Level Code and Proof-Preserving Program Transformations, Thesis in Informatics and System Engineering C43, 172 pp. Tallinn Univ. of Techn., 2008. thesis at TUT digital library
Defense at Tallinn Univ. of Techn., 14 Nov. 2008. Supervisors T. Uustalu, E. Tõugu (Inst. of Cybernetics), opponents B. Fischer (Univ. of Southampton), D. Sands (Chalmers Univ. of Techn. and Göteborg Univ.).

PhD defenses 2010

V. Vojdani. Static Data Race Analysis of Heap-Manipulating C Programs, v. 64 of Diss. Math. Univ. Tartuensis, 137 pp. Univ. of Tartu, 2010. handle: 10062/15866
Defense at Univ. of Tartu, 10 Dec. 2010. Supervisors V. Vene (Univ. of Tartu), H. Seidl (Techn. Univ. München), opponents A. Mycroft (Univ. of Cambridge), K. Nakata (Inst. of Cybernetics).

Last update 31 January 2012