Programming languages and systems (PLS)
Key persons
T. Uustalu, V. Vene, S. Capobianco, J. Chapman, K. Nakata,
H. Nestra, H. Tamm, V. Vojdani
Postdocs
W. Jeltsch
Logic and semantics research
group of IoC, Programming
languages and systems research group of UT
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, Scopus: 2-s2.0-44049100677)
- 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 (Scopus:
2-s2.0-59249096516)
- 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, Scopus: 2-s2.0-49349090106)
- 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, Scopus: 2-s2.0-77950908724)
- 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, Scopus: 2-s2.0-44849099202)
- 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
on 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 on workshop's
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 (Scopus:
2-s2.0-44649112368)
- 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, Scopus: 2-s2.0-58049117608)
- 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, Scopus: 2-s2.0-67749102278)
- 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, Scopus 2-s2.0-70349747040)
- 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, Scopus: 2-s2.0-70649091000)
- 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, Scopus: 2-s2.0-71049177308)
- 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 (Scopus: 2-s2.0-67650691954)
- 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, Scopus: 2-s2.0-67749098007)
- 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, Scopus: 2-s2.0-84865234315)
- 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, Scopus: 2-s2.0-70350325123)
- 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, Scopus: 2-s2.0-69349090631)
- 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, Scopus: 2-s2.0-77956300109)
- 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, Scopus: 2-s2.0-69349104944)
- 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, Scopus: 2-s2.0-70350302848)
- 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, Scopus: 2-s2.0-70649099069)
- 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, Scopus: 2-s2.0-67349184519)
- 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, Scopus: 2-s2.0-77951455012)
- 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, Scopus: 2-s2.0-77957315717)
- 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, Scopus: 2-s2.0-78650735634)
- 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, Scopus: 2-s2.0-77249176655)
- S. Capobianco, T. Toffoli. Dissipative CA computation without
power sources? J. of Cellular Automata, v. 5, n. 3,
pp. 169-183, 2010. article
on publisher's website (WOS:
000276557000002, Scopus: 2-s2.0-77952580122)
- 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 in
DORIA, article in
HAL (Scopus: 2-s2.0-84878730852)
- 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. doi:
10.1145/1863597 (Scopus:
2-s2.0-78249249271)
- 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, Scopus: 2-s2.0-78249243417)
- 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, Scopus: 2-s2.0-79551677425)
- 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, Scopus: 2-s2.0-77949359395)
- 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 in 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 (WOS:
000306306500004, Scopus: 2-s2.0-84943595034)
- 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, Scopus: 2-s2.0-77951265253)
- 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 (Scopus:
2-s2.0-84954532658)
- 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, Scopus: 2-s2.0-77953790515)
- 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, ERTS2 2010 (Toulouse,
May 2010), 10 pp. SIA, 2010. article on 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, Scopus: 2-s2.0-84865764898)
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 (Scopus:
2-s2.0-79960719786)
- 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, Scopus: 2-s2.0-79957874698)
- 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 (Scopus:
2-s2.0-79959324332)
- J. Garrigue, K. Nakata. Path resolution for nested
recursive modules. Higher-Order and Symbolic Computation,
v. 24, n. 3, pp. 207-237, 2011. doi:
10.1007/s10990-012-9083-6 (Scopus:
2-s2.0-84865234315)
- 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 (WOS:
000304282000058, Scopus: 2-s2.0-81455159323)
- 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 (WOS:
000298294500058, Scopus: 2-s2.0-84863383614)
- 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 (Scopus:
2-s2.0-79951996822)
- J. Kabanov. Reloading von Java-Klassen... mit Classloadern,
HotSwap und JRebel. Java-Magazin, v. 2011, n. 3, pp. 104-109,
2011.
- 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, Scopus: 2-s2.0-79958851255)
- 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. Open
Publishing Assoc., 2011. doi:
10.4204/eptcs.66.12 (Scopus:
2-s2.0-84954525746)
- 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 (Scopus:
2-s2.0-84055193127)
- 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. (WOS:
000328999800003, Scopus: 2-s2.0-84869845905)
- 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. doi:
10.2298/fuee1103325p
- 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 (Scopus:
2-s2.0-84954454791)
- 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, Scopus: 2-s2.0-79952035452)
- 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, Scopus: 2-s2.0-79251539904)
- 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 (Scopus:
2-s2.0-79952433647)
- 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 (Scopus:
2-s2.0-79959297218)
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), v. 7213 of
Lect. Notes in Comput. Sci., pp. 74-88. Springer, 2012. doi:
10.1007/978-3-642-28729-9_5 (WOS:
000342756900005, Scopus: 2-s2.0-84859138343)
- K. Apinis, H. Seidl, V. Vojdani. Side-effecting
constraint systems: a Swiss army knife for program analysis. In
R. Jhala, A. Igarashi, eds.,
Proc. of 10th Asian Symp. on Programming Languages and Systems,
APLAS 2012 (Kyoto, Dec. 2012), v. 7705 of Lect. Notes in
Comput. Sci., pp. 157-172. Springer, 2012. doi:
10.1007/978-3-642-35182-2_12 (Scopus:
2-s2.0-84872243482)
- Z. Ariola, P. Downen, H. Herbelin, K. Nakata, A. Saurin.
Classical call-by-need sequent calculi: the unity of semantic
artifacts. 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. 32-46. Springer, 2012. doi:
10.1007/978-3-642-29822-6_6 (WOS:
000440210000006, Scopus: 2-s2.0-84861726894)
- 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 (WOS:
000315381600014, Scopus: 2-s2.0-84868152421)
- M. Bordin, T. Näks, A. Toom, M. Pantel. Compilation of
heterogeneous models: motivations and challenges. In Proc. of 6th
Europ. Conf. on Embedded Real-Time Software and Systems,
ERTS2 2012 (Toulouse, Feb. 2012), 10 pp. SIA, 2012. article on
conference website
- J. Brzozowski, H. Tamm. Quotient complexities of atoms of
regular languages. In H.-C. Yen, O. H. Ibarra, eds., Proc. of 16th
Int. Conf. on Developments in Language Theory, DLT 2012 (Taipei,
August 2012), v. 7410 of
Lect. Notes in Comput. Sci., pp. 50-61. Springer, 2012. doi:
10.1007/978-3-642-31653-1_6 (WOS:
000440210900006, Scopus: 2-s2.0-84865024625)
- S. Capobianco, T. Toffoli. Conserved quantities in discrete
dynamics: what can be recovered from Noether's theorem, how, and why?
Nat. Comput., v. 11, n. 4, pp. 565-577, 2012. doi:
10.1007/s11047-012-9336-7 (WOS:
000312130900003, Scopus: 2-s2.0-84864509600)
- J. Chapman, P. B. Levy, eds. Proc. of 4th Wksh. on
Mathematically Structured Functional Programming, MSFP 2012
(Tallinn, March 2012), v. 76 of Electron. Proc. in
Theor. Comput. Sci., 177 pp. Open Publishing Assoc., 2012. doi: 10.4204/eptcs.76
(Scopus: 2-s2.0-84958726191)
- A. Dieumegard, A. Toom, M. Pantel. Model-based formal
specification of a DSL library for a qualified code generator. In
Proc. of 2012 Wksh. on OCL and Textual Modelling, OCL 2012
(Innsbruck, Sept. 2012), pp. 61-62. ACM Press, 2012. doi:
10.1145/2428516.2428527 (Scopus:
2-s2.0-84873332095)
- A. Herz, K. Apinis. Class-modular, class-escape and
points-to analysis for object-oriented languages. In A. Goodloe,
S. Person, eds., Proc. of 4th NASA Formal Methods Symp.,
NFM 2012 (Norfolk, VA, Apr. 2012), v. 7226 of
Lect. Notes in Comput. Sci., pp. 106-119. Springer, 2012. doi:
10.1007/978-3-642-28891-3_11 (Scopus:
2-s2.0-84859465102)
- W. Jeltsch. Towards a common categorical semantics for
linear-time temporal logic and functional reactive programming. In
U. Berger, M. Mislove, eds., Proc. of 28th Conf. on Mathematical
Foundations of Programming Semantics, MFPS XXVIII (Bath, June
2012), v. 286 of Electron. Notes in Theor. Comput. Sci.,
pp. 229-242. Elsevier, 2012. doi:
10.1016/j.entcs.2012.08.015 (Scopus:
2-s2.0-84873472699)
- T. Tamme. Logic in Estonia. In A. Schumann, ed., Logic in
Central and Eastern Europe: History, Science, and Discourse,
pp. 166-171. Univ. Press of America, 2012.
- 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 (WOS:
000440210000025, Scopus: 2-s2.0-84861726904)
- 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),
v. 77 of Electron. Proc. in Theor. Comput. Sci.,
pp. 55-61. Open Publishing Assoc., 2012. doi:
10.4204/eptcs.77.8 (Scopus:
2-s2.0-84954560593)
- B. van der Merwe, H. Tamm, L. van Zijl. Minimal DFA for
symmetric difference NFA. In M. Kutrib, N. Moreira, R. Reis, eds.,
Proc. of 14th Int. Wksh. on Descriptional Complexity of Formal
Systems, DCFS 2012 (Braga, July 2012), v. 7386 of
Lect. Notes in Comput. Sci., pp. 307-318. Springer, 2012. doi:
10.1007/978-3-642-31623-4_24 (WOS:
000440496400024, Scopus: 2-s2.0-84864831410)
Publications 2013
- D. Ahman, S. Staton. Normalization by evaluation and
algebraic effects. In D. Kozen, M. Mislove, eds., Proc. of 29th
Conf. on Mathematical Foundations of Programming Semantics, MFPS XXIX
(New Orleans, LA, June 2013), Electron. Notes in
Theor. Comput. Sci., v. 298, pp. 51-69. Elsevier, 2013. doi:
10.1016/j.entcs.2013.09.007 (Scopus:
2-s2.0-84888034421)
- 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 (Scopus:
2-s2.0-84877657005)
- K. Apinis, H. Seidl, V. Vojdani. How to combine
widening and narrowing for non-monotonic systems of equations. In
Proc. of 34th ACM SIGPLAN Conf. on Programming Language Design and
Implementation, PLDI '13 (Seattle, WA, June 2013),
pp. 377-386. ACM Press, 2013. doi:
10.1145/2491956.2462190 (Scopus:
2-s2.0-84883119385)
- K. Apinis, H. Seidl, V. Vojdani. How to combine
widening and narrowing for non-monotonic systems of equations. In
ACM SIGPLAN Notices, v. 48, n. 6, pp. 377-387, 2013. doi:
10.1145/2499370.2462190 (WOS:
000321865400036, Scopus: 2-s2.0-84880094683)
- J. Brzozowski, H. Tamm. Complexity of atoms of regular
languages. Int. J. of Found. of Comput. Sci., v. 24, n. 7,
pp. 1009-1027, 2013. doi:
10.1142/s0129054113400285 (WOS:
000332114100006, Scopus: 2-s2.0-84897656838)
- S. Capobianco, P. Guillon, J. Kari. Surjective cellular
automata far from the Garden of Eden. Discr. Math. and
Theor. Comput. Sci., v. 15, n. 3, pp. 41-60, 2013. article
at publisher's website (WOS:
000327036900005, Scopus: 2-s2.0-84887845542)
- 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 (WOS:
000440498800007, Scopus: 2-s2.0-84893051683)
- I. Hasuo, K. Nakata, T. Uustalu, eds. Coinduction
for Computation Structures and Programming Languages (Oct. 2013),
v. 2013-11 of
NII Shonan Meeting Reports, 16 pp. Nat. Inst. of Inform.,
2013. report
on NII website
- H. Im, K. Nakata, S. Park. Contractive signatures with
recursive types, type parameters, and abstract types. In F. V. Fomin,
R. Freivalds, M. Z. Kwiatkowska, D. Peleg, eds., Proc. of 40th
Int. Coll. on Automata, Languages and Programming, ICALP 2013
(Riga, July 2013), Part II, v. 7966 of
Lect. Notes in Comput. Sci., pp. 299-311. Springer, 2013. doi:
10.1007/978-3-642-39212-2_28 (WOS:
000342684100028, Scopus: 2-s2.0-84880288390)
- W. Jeltsch. Temporal logic with "until", functional
reactive programming with processes, and concrete process
categories. In Proc. of 7th Wksh. on Programming Languages Meets
Program Verification, PLPV '13 (Rome, Jan. 2013),
pp. 69-78. ACM Press, 2013. doi:
10.1145/2428116.2428128 (Scopus:
2-s2.0-84873438971)
- R. Matthes, T. Uustalu, guest eds. Theor. Inform. and
Appl., v. 47, n. 1 (Selected Papers from 6th Wksh. on Fixed Points
in Comput. Sci., FICS '09, Coimbra, Sept. 2009), pp. 1-132,
2013. doi:
10.1051/ita/2012026 (WOS:
000315619400001, Scopus: 2-s2.0-84877657005)
- G. Morrisett, T. Uustalu, eds. Proc. of 18th ACM SIGPLAN
Int. Conf. on Functional Programming, ICFP' 13 (Boston, MA,
Sept. 2013), xii+469 pp. ACM Press, 2013. doi: 10.1145/2500365
(Scopus: 2-s2.0-84887206202)
- G. Morrisett, T. Uustalu, guest eds. ACM SIGPLAN
Notices, v. 48, n. 9 (Proc. of ICFP '13), xii+469 pp.,
2013. doi:
10.1145/2544174 (Scopus:
2-s2.0-84888634338)
- K. Nakata, A. Saar. Compiling cooperative task
management to continuations. In F. Arbab, M. Sirjani, eds.,
Revised Selected Papers from 5th Int. Conf. on Fundamentals of
Software Engineering, FSEN '13 (Tehran, Apr. 2013), v. 8161
of Lect. Notes in Comput. Sci., pp. 95-110. Springer, 2013. doi:
10.1007/978-3-642-40213-5_7 (WOS:
000440497900007, Scopus: 2-s2.0-84886384579)
- H. Nestra. On slicing of programs with input statements. In
Z. Liu, J. Woodcock, H. Zhu, eds., Proc. of 10th Int. Coll. on
Theoretical Aspects of Computing, ICTAC 2013 (Shanghai,
Sept. 2013), v. 8049 of Lect. Notes in Comput. Sci.,
pp. 282-300. Springer, 2013. doi:
10.1007/978-3-642-39718-9_17 (Scopus:
2-s2.0-84885004089)
- W. Rafnsson, K. Nakata, A. Sabelfeld. Securing class
initialization in Java-like languages. IEEE Trans. on Dependable
and Secure Computing, v. 10, n. 1, pp. 1-13, 2013. doi:
10.1109/tdsc.2012.73 (WOS:
000312779000001, Scopus: 2-s2.0-84872013232)
- O. Šelajev, R. Raudjärv, J. Kabanov. Static analysis for
dynamic updates. In Proc. of 9th Central and Eastern European
Software Engineering Conf. in Russia, CEE-SECR '13 (Moscow,
Oct. 2013), ACM Int. Conf. Proc. Series, article 7. ACM
Press, 2013. doi:
10.1145/2556610.2556620 (Scopus:
2-s2.0-84894600008)
- 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 (Scopus:
2-s2.0-84954516018)
- T. Uustalu, J. Vain, eds. Abstracts of 25th
Nordic Wksh. on Programming Theory, NWPT 2013 (Tallinn,
Nov. 2013), vi+75 pp. Inst. of Cybern., 2013. volume on workshop's
website
Publications 2014
- A. Abel, J. Chapman. Normalization by evaluation in the
delay monad: a case study for coinduction via copatterns and sized
types. 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. 51-67. Open Publishing Assoc., 2014. doi:
10.4204/eptcs.153.4 (Scopus:
2-s2.0-84938794091)
- 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 (WOS:
000347714800024, Scopus: 2-s2.0-84908291183)
- 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 (Scopus:
2-s2.0-84908384283)
- 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 (Scopus:
2-s2.0-84907731424)
- T. Altenkirch, J. Chapman, T. Uustalu. Relative
monads formalised. J. of Formalized Reasoning, v. 7, n. 1,
pp. 1-43, 2014. doi:
10.6092/issn.1972-5787/4389 (Scopus:
2-s2.0-84904630409)
- J. Brzozowski, H. Tamm. Theory of
átomata. Theor. Comput. Sci., v. 539, pp. 13-27, 2014. doi:
10.1016/j.tcs.2014.04.016 (WOS:
000338598500002, Scopus: 2-s2.0-84926689142)
- A. Dieumegard, A. Toom, M. Pantel. A software product line
approach for semantic specification of block libraries in dataflow
languages. In Proc. of 18th Int. Software Product Line Conference,
SPLC 2014 (Florence, Sept. 2014), v. 1, ACM
Int. Conf. Proc. Series, pp. 217-226. ACM Press, 2014. doi:
10.1145/2648511.2648534 (Scopus:
2-s2.0-84907814299)
- A. Dieumegard, A. Toom, M. Pantel. Formal specification of
block libraries in dataflow languages. In Proc. of 7th Europ.
Conf. on Embedded Real-Time Software and Systems, ERTS2 2014
(Toulouse, Feb. 2014), 10 pp. SIA, 2014. article
on conference website
- D. Firsov, T. Uustalu. Certified CYK parsing of
context-free languages. J. of Log. and Algebr. Methods in
Program., v. 83, n. 5-6, pp. 459-468, 2014. doi:
10.1016/j.jlamp.2014.09.002 (WOS:
000345179400006, Scopus: 2-s2.0-84938688808)
- D. Ilik, K. Nakata. A direct version of Veldman's proof of
open induction on Cantor space via delimited control operators. 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. 188-201. Dagstuhl Publishing,
2014. doi:
10.4230/lipics.types.2013.188 (Scopus:
2-s2.0-84907737679)
- W. Jeltsch. An abstract categorical semantics for
functional reactive programming with processes. In Proc. of 8th
Wksh. on Programming Languages Meets Program Verification,
PLPV '14 (San Diego, CA, Jan. 2014), pp. 47-58. ACM Press,
2014. doi:
10.1145/2541568.2541573 (Scopus:
2-s2.0-84897676565)
- W. Jeltsch. Categorical semantics for functional reactive
programming with temporal recursion and corecursion. 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. 127-142. Open Publishing Assoc., 2014. doi:
10.4204/eptcs.153.9 (Scopus:
2-s2.0-84938791864)
- J. Kabanov, V. Vene. A thousand years of
productivity: the JRebel story. Software: Practice and
Experience, v. 44, n. 1, pp. 105-127, 2014. doi: 10.1002/spe.2158
(WOS: 000328419600005, Scopus:
2-s2.0-84890553356)
- M. Schwarz, H. Seidl, V. Vojdani, K. Apinis. Precise
analysis of value-dependent synchronization in programs with priority
scheduling. In K. L. McMillan, X. Rival, eds., Proc. of 15th
Int. Conf. on Verification, Model Checking and Abstract
Interpretation, VMCAI 2014 (San Diego, CA, Jan. 2014),
pp. 21-38. Springer, 2014. doi:
10.1007/978-3-642-54013-4_2 (WOS:
000354781700002, Scopus: 2-s2.0-84893355951)
- H. Seidl, K. Apinis, V. Vojdani. Frameworks for
interprocedural analysis of concurrent programs. In O. Grumberg,
H. Seidl, M. Irlbeck, eds., Lectures from NATO ASI on Software
Systems Safety (Marktoberdorf, July/Aug. 2013), v. 36 of
NATO Science for Peace and Security, Series D: Information and
Communication Security, pp. 309-347. IOS Press, 2014. doi:
10.3233/978-1-61499-385-8-309
- A. Toom, A. Dieumegard, M. Pantel. Specifying and verifying
model transformations for certified systems using transformation
models. In Proc. of 7th Europ Conf. on Embedded Real-Time
Software and Systems, ERTS2 2014 (Toulouse, Feb. 2014), 10
pp. SIA, 2014. article
on conference website
- 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 (Scopus:
2-s2.0-84927626955)
Publications 2015
- G. Amato, F. Scozzari, H. Seidl, K. Apinis,
V. Vojdani. Efficiently intertwining widening and
narrowing. Sci. of Comput. Program., v. 120, pp. 1-24, 2016. doi:
10.1016/j.scico.2015.12.005 (WOS:
000372693400001, Scopus: 2-s2.0-84959552431)
- K. Apinis, H. Seidl, V. Vojdani. Enhancing top-down
solving with widening and narrowing. In C. W. Probst, C. Hankin,
R. R. Hansen, eds., Semantics, Logics and Calculi: Essays Dedicated
to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their
60th Birthdays, v. 9560 of Lect. Notes in Comput. Sci.,
pp. 272-288. Springer, 2016. doi:
10.1007/978-3-319-27810-0_14 (WOS:
000381922800014, Scopus: 2-s2.0-84955293729)
- C. Artho, E. B. Johnsen, M. Leucker, K. Nakata,
eds. Static Analysis Meets Runtime Verification (March 2015),
v. 2015-5 of
NII Shonan Meeting Reports, 12 pp. Nat. Inst. of Inform.,
2015. report on NII website
- 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 (WOS:
000353193000010, Scopus: 2-s2.0-84927621403)
- R. Bubel, C. C. Din, R. Hähnle, K. Nakata. A dynamic logic
with traces and coinduction. In H. de Nivelle, ed., Proc. of 24th
Int. Conf. on Automated Reasoning with Analytic Tableaux and Related
Methods, TABLEAUX 2015 (Wroclaw, Sept. 2015), v. 9323 of
Lect. Notes in Artif. Intell., pp. 307-322. Springer, 2015. doi:
10.1007/978-3-319-24312-2_21 (WOS:
000366125200024, Scopus: 2-s2.0-84950127231)
- S. Capobianco, J. Kari, S. Taati. Post-surjectivity and
balancedness of cellular automata over groups. In J. Kari, I. Törmä,
M. Szabados, eds., Exploratory Papers of 21st Int. Wksh. on
Cellular Automata and Discrete Complex Systems, AUTOMATA 2015 (Turku,
June 2015), v. 24 of TUCS Lecture Notes,
pp. 31-38. Turku Centre for Computer Science, 2015.
- J. Chapman, T. Uustalu, N. Veltri.
Quotienting the delay monad by weak bisimilarity. 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 (WOS:
000366212700008, Scopus: 2-s2.0-84952056543)
- 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 (Scopus:
2-s2.0-84966783955)
- 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 (Scopus:
2-s2.0-84991614482)
- 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 (WOS:
000353193000009, Scopus: 2-s2.0-84927614414)
- N. Swamy, T. Uustalu, guest eds. J. of
Funct. Program., v. 25, articles e10, e12, e18, v. 26, articles
e1, e2, e4 (collection for 18th ACM SIGPLAN Int. Conf. on Functional
Programming, ICFP 2013, Boston, MA, Sept. 2013), 2015-2016. collection
on publisher's website
- H. Tamm. Generalization of the double-reversal method of
finding a canonical residual finite state automaton. In J. Shallit,
A. Okhotin, eds., Proc. of 17th Int. Wksh. on Descriptional
Complexity of Formal Systems, DCFS 2015 (Waterloo, ON, June
2015), v. 9118 of Lect. Notes in Comput. Sci.,
pp. 268-279. Springer, 2015. doi:
10.1007/978-3-319-19225-3_23 (Scopus:
2-s2.0-84949008979)
- T. Uustalu, ed. Abstracts of 21st Int. Conf. on Types
for Proofs and Programs, TYPES 2015 (Tallinn, May 2015), vii+82
pp. Inst. of Cybernetics, 2015. volume on publisher's
website
- T. Uustalu. A divertimento on MonadPlus and
nondeterminism. J. of Log. and Algebr. Methods in Program.,
v. 85, n. 5, part 2, pp. 1086-1094, 2016. doi:
10.1016/j.jlamp.2016.06.004 (WOS:
000384382000018, Scopus: 2-s2.0-84978390183)
- T. Uustalu, ed. Proc. of 21st Int. Conf. on Types
for Proofs and Programs, TYPES 2015 (Tallinn, May 2015),
Leibniz Int. Proc. in Inform., Dagstuhl Publishing, in
preparation.
- 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. Elsevier, 2015. doi:
10.1016/j.entcs.2015.12.024 (WOS:
000372714600024, Scopus: 2-s2.0-84951730054)
- T. Uustalu, J. Vain, guest eds. J. of Log. and
Algebr. Methods in Program., v. 85, n. 6 (Special Issue for 25th
Nordic Wksh. in Programming Theory, NWPT 2013, Tallinn,
Nov. 2013), pp. 1109-1317, 2016. doi:
10.1016/j.jlamp.2016.10.004
- N. Veltri. Two set-based implementations of quotients in
type theory. In J. Nummenmaa, O. Sievi-Korte, E. Mäkinen, eds.,
Proc. of 14th Symp. on Programming Languages and Software Tools,
SPLST '15 (Tampere, Oct. 2015), v. 1525 of CEUR
Wksh. Proc., pp. 194-205. RWTH Aachen, 2015. article on publisher's
website (Scopus:
2-s2.0-84962598967)
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 in TUT DL
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).
PhD defenses 2013
- J. Kabanov. Towards a More Productive Java EE
Ecosystem, v. 84 of
Diss. Math. Univ. Tartuensis, 151 pp. Univ. of Tartu, 2013. handle: 10062/29302
Defense at Univ. of Tartu, 5 April 2013. Supervisor V. Vene (Univ. of
Tartu), opponents R. N. Horspool (Univ. of Victoria, BC), T. Tammet
(Tallinn Univ. of Techn.).
PhD defenses 2014
- K. Apinis. Frameworks for Analyzing Multi-Threaded
C, v+126 pp. Technische Univ. München, 2014.
Defense at Technische Univ. München, June 2014. Supervisor H. Seidl
(Technische Univ. München). thesis at
TUM
Last update 11 August 2018