Logic and Semantics Group: Publications

Publications 2002

  1. G. Barthe, T. Uustalu. CPS translating inductive and coinductive types. 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 (Scopus: 2-s2.0-0036041754) 3.1
  2. G. Barthe, T. Uustalu. CPS translating inductive and coinductive types. ACM SIGPLAN Notices, v. 37, n. 3, pp. 131-142, 2002. doi: 10.1145/509799.503043 (WOS: 000175149200014) 1.1
  3. 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 (WOS: 000173096200011, Scopus: 2-s2.0-0037028519) 1.1
  4. 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, 2002. (WOS: 000181626000009) 3.1
  5. J. Vain, T. Uustalu, eds., Abstracts of 14th Nordic Wksh. on Programming Theory (Tallinn, Nov. 2002), 101 pp. Inst. of Cybern., 2002. 4.2

Publications 2003

  1. 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 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 (WOS: 000183067500004, Scopus: 2-s2.0-35248899419) 1.1
  2. 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 3.1
  3. 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., pp. 191-205. Elsevier, 2003. doi: 10.1016/s1571-0661(04)80639-x (Scopus: 2-s2.0-0942302122) 1.1
  4. 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 (WOS: 000180379400005, Scopus: 2-s2.0-0037445581) 1.1
  5. S. Tupailo. Epsilon-substitution method for Δ11-CR: a constructive termination proof. Log. J. of IGPL, v. 11, n. 3, pp. 367-377, 2003. doi: 10.1093/jigpal/11.3.367 (WOS: 000202948500004) 1.1
  6. 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. 3.2
  7. T. Uustalu. Generalizing substitution. Theor. Inf. and Appl., v. 37, n. 4, pp. 315-336, 2003. doi: 10.1051/ita:2003022 (WOS: 000220666900004, Scopus: 2-s2.0-0942267770) 1.1
  8. 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, Berlin, 2003. doi: 10.1007/3-540-39185-1_17 (WOS: 000183489200017, Scopus: 2-s2.0-32144458820) 1.1
  9. J. Vain, T. Uustalu, guest eds., Proc. of Estonian Acad. of Sci., Phys., Math., v. 52, n. 4 (Selected Papers from 14th Nordic Wksh. on Programming Theory, NWPT '02, Tallinn, Nov. 2002), 2003. 4.1

Publications 2004

  1. 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 (WOS: 000189484700019, Scopus: 2-s2.0-35048841111) 1.1
  2. 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 (WOS: 000228425800004, Scopus: 2-s2.0-84855618972) 1.1
  3. 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 (Scopus: 2-s2.0-10444237255) 1.1
  4. 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 (WOS: 000225386700003, Scopus: 2-s2.0-8344279624) 1.1
  5. 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 (WOS: 000224947700021, Scopus: 2-s2.0-35048864529) 1.1
  6. 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. 3.4
  7. 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 (WOS: 000224616300008, Scopus: 2-s2.0-4944265294) 1.1
  8. S. Tupailo. On the intuitionistic strength of monotone inductive definitions. J. of Symb. Logic, v. 69, n. 3, pp. 790-798, 2004. doi: 10.2178/jsl/1096901767 (WOS:000223564800010, Scopus: 2-s2.0-4644354121) 1.1

Publications 2005

  1. 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 (WOS: 000227699100002, Scopus: 2-s2.0-13644281245) 1.1
  2. 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 (Scopus: 2-s2.0-84876767327) 3.1
  3. 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 (WOS: 000232089200028, Scopus: 2-s2.0-33745211455) 1.1
  4. 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 (WOS: 000233547100032, Scopus: 2-s2.0-26844509701) 1.1
  5. 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. 3.4
  6. 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 (Scopus: 2-s2.0-32044449386) 3.1
  7. 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. 3.4
  8. 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. 3.4
  9. 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 (WOS: 000232351300012, Scopus: 2-s2.0-24944434990) 1.1
  10. 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 (WOS: 000233897200001, Scopus: 2-s2.0-33646744717) 1.1
  11. V. Vene, M. Meriste, eds., Proc. of 9th Symp. on Programming Languages and Software Tools, SPLST 2005 (Tartu, Sept. 2005), 234 pp. Univ. of Tartu, 2005. 4.2
  12. 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 (Scopus: 2-s2.0-33646055534) 4.1

Publications 2006

  1. 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 (WOS: 000236940300009, Scopus: 2-s2.0-33745662871) 1.1
  2. 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 (WOS: 000237854100002, Scopus: 2-s2.0-84855190252) 1.1
  3. 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. 3.4
  4. 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 (Scopus: 2-s2.0-33747266802) 1.1
  5. 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. 3.1
  6. 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 (Scopus: 2-s2.0-33744987872) 1.1
  7. 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. 3.4
  8. 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 (Scopus: 2-s2.0-33746038922) 4.1
  9. 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 (WOS: 000239422700015, Scopus: 2-s2.0-33746035705) 1.1
  10. 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 (WOS: 000241718500003, Scopus: 2-s2.0-33749629455) 1.1
  11. 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 4.1
  12. M. Rathjen, S. Tupailo. Characterizing the interpretation of set theory in Martin-Löf type theory. Ann. of Pure and Appl. Log., v. 141, n. 3, pp. 442-471, 2006. doi: 10.1016/j.apal.2005.12.008 (WOS: 000238504800010, Scopus: 2-s2.0-33747088308) 1.1
  13. 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 (Scopus: 2-s2.0-33646384378) 1.1
  14. 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 Inf. Technol., pp. 27-39. Australian Comput. Soc., 2006. article at ACM DL (Scopus: 2-s2.0-84863582481) 3.1
  15. 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 (WOS: 000236480300026, Scopus: 2-s2.0-33745141516) 1.1
  16. 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 (WOS: 000241545800011, Scopus: 2-s2.0-33749265349) 1.1
  17. 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 (Scopus: 2-s2.0-33746059789) 4.1
  18. 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 (WOS: 000241443300005, Scopus: 2-s2.0-33751405362) 1.1

Publications 2007

  1. 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 (WOS: 000247666400010, Scopus: 2-s2.0-34548816983) 3.1
  2. 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 (WOS: 000248143000053, Scopus: 2-s2.0-38149047520) 3.1
  3. B. Jacobs, T. Uustalu. Semantics of grammars and attributes via initiality. In E. Barendsen, V. Capretta, H. Geuvers, M. Niqui, eds., Reflections on Type Theory, Lambda-Calculus, and the Mind: Essays Dedicated to Henk Barendregt on the Occasion of His 60th Birthday, pp. 181-196. Radboud Univ. Nijmegen, 2007. article on publisher's webpage 3.2
  4. 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 (WOS: 000245836600006, Scopus: 2-s2.0-33947145531) 1.1
  5. 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 (Scopus: 2-s2.0-34547193722) 1.1
  6. 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 (WOS: 000247909100038, Scopus: 2-s2.0-34548084924) 3.1
  7. S. Tupailo. Fixpoints of models constructions. Logique et Analyse (Nouvelle Série), v. 50, n. 197, pp. 63-78, 2007. article on publisher's website (WOS: 000256449200004, Scopus: 2-s2.0-60950566482) 1.1
  8. S. Tupailo. Monotone inductive definitions and consistency of New Foundations. In C. Dimitracopoulos, L. Newelski, D. Normann, J. R. Steel, eds., Proc. of Ann. Europ. Summer Meeting of ASL, Logic Coll. 2005 (Athens, July/Aug. 2005), v. 28 of Lect. Notes in Log., pp. 255-272. Cambridge Univ. Press, 2007. doi: 10.1017/cbo9780511546464.016 3.1
  9. T. Uustalu, V. Vene. Comonadic functional attribute evaluation. In M. van Eekelen, ed., Trends in Functional Programming 6, pp. 145-162. Intellect, 2007. 3.1

Publications 2008

  1. 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 2.3
  2. A. Saabas, T. Uustalu. Program and proof optimizations with type systems. J. of Log. and Algebr. 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) 1.1
  3. 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) 3.1
  4. 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) 1.1
  5. 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 3.4
  6. 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 4.2
  7. 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) 1.1
  8. 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) 3.1
  9. 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) 5.1

Publications 2009

  1. 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) 1.1
  2. S. Capobianco. On the induction operation for shift subspaces and cellular automata as presentations of dynamical systems. Inf. and Comput., v. 207, n. 11, pp. 1169-1180, 2009. doi: 10.1016/j.ic.2009.02.006 (WOS: 000271169800006, Scopus 70349747040) 1.1
  3. 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. 3.4
  4. 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. 3.4
  5. 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) 3.1
  6. 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) 3.1
  7. 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) 3.1
  8. 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 on publisher's website 4.2
  9. 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) 4.1
  10. 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) 1.1
  11. 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) 3.1
  12. 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) 3.1
  13. A. Saabas, T. Uustalu. Proof optimization for partial redundancy elimination. J. of Log. 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) 1.1
  14. S. Tupailo. Consistency of strictly impredicative NF. In C. Drossos, P. Peppas, C. Tsinakis, eds., Proc. of 7th Panhellenic Logic Symp. (Patras, July 2009), pp. 179-186. Patras Univ. Press, 2009. 3.4
  15. S. Tupailo. NF and indiscernibles in NF. In M. Crabbé, T. Forster, eds., Proc. of 70th Anniversary NF Meeting in Cambridge (May 2007), v. 16 of Cahiers du Centre de Logique, pp. 99-107. Academia-Bruylant, 2009. 1.2
  16. 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. issue on publisher's website (WOS: 000266671700001, Scopus: 2-s2.0-67349184519) 4.1

Publications 2010

  1. 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) 3.1
  2. T. Altenkirch, T. Uustalu, guest eds. Fundam. Inf., 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) 4.1
  3. 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) 3.1
  4. S. Capobianco, T. Toffoli. Dissipative CA computation without power sources? J. of Cell. Autom., v. 5, n. 3, pp. 169-183, 2010. article on publisher's website (WOS: 000276557000002, Scopus: 2-s2.0-77952580122) 1.1
  5. 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) 3.1
  6. 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: 78249249271) 4.1
  7. 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) 3.1
  8. 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) 1.1
  9. 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 3.4
  10. 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) 3.1
  11. 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) 3.1
  12. 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) 3.1
  13. 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) 3.1
  14. 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 3.4
  15. 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. 1.3
  16. S. Tupailo. Consistency of strictly impredicative NF and a little more. J. of Symb. Logic, v. 75, n. 4, pp. 1326-1338, 2010. doi: 10.2178/jsl/1286198149 (WOS: 000285493000010, Scopus: 2-s2.0-78951472510) 1.1
  17. 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 in HAL 3.4
  18. 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) 4.1

Publications 2011

  1. 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) 3.1
  2. 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) 1.1
  3. 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. 3.4
  4. 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) 3.1
  5. J. Garrigue, K. Nakata. Path resolution for nested recursive modules. High.-Order and Symb. Comput., v. 24, n. 3, pp. 207-237, 2011. doi: 10.1007/s10990-012-9083-6 (Scopus: 2-s2.0-84865234315) 1.1
  6. 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) 3.1
  7. 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) 1.1
  8. 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) 3.1
  9. 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) 3.1
  10. 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) 3.1
  11. 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) 1.1
  12. 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) 3.1

Publications 2012

  1. 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) (ETAPS 2012 best paper award nomination) 3.1
  2. 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 (Scopus: 2-s2.0-84861726894) 3.1
  3. 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) 1.1
  4. 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 3.4
  5. 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 (Scopus: 2-s2.0-84865024625) 3.1
  6. 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) 1.1
  7. 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)4.1
  8. 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) 3.1
  9. 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) 1.1
  10. 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 (Scopus: 2-s2.0-84861726904) 3.1
  11. 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) 3.1
  12. 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 (Scopus: 2-s2.0-84864831410) 3.1

Publications 2013

  1. 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), v. 298 of Electron. Notes in Theor. Comput. Sci., pp. 51-69. Elsevier, 2013. doi: 10.1016/j.entcs.2013.09.007 (Scopus: 2-s2.0-84888034421) 1.1
  2. 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) 1.1
  3. 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) 1.1
  4. 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) 1.1
  5. 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 (Scopus: 2-s2.0-84893051683) 3.1
  6. 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 Inf., 2013. report on NII website 4.2
  7. 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) 3.1
  8. 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) 3.1
  9. R. Matthes, T. Uustalu, guest eds. Theor. Inf. 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) 4.1
  10. 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) 4.1
  11. 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) 4.1
  12. 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 (Scopus: 2-s2.0-84886384579) 3.1
  13. 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) 1.1
  14. 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) 3.1
  15. 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 4.2

Publications 2014

  1. 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) 3.1
  2. 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) 1.1
  3. 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. 10.1016/j.entcs.2014.10.003 (Scopus: 2-s2.0-84908384283) 1.1
  4. 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 Inf., pp. 1-23. Dagstuhl Publishing, 2014. doi: 10.4230/lipics.types.2013.1 (Scopus: 2-s2.0-84907731424) 3.1
  5. 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 (Scopus: 2-s2.0-84904630409) 1.1
  6. 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) 1.1
  7. 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) 3.1
  8. 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 3.4
  9. 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) 1.1
  10. 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 Inf., pp. 188-201. Dagstuhl Publishing, 2014. doi: 10.4230/lipics.types.2013.188 (Scopus: 2-s2.0-84907737679) 3.1
  11. 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) 3.1
  12. 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) 3.1
  13. 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 3.4
  14. 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) 3.1

Publications 2015

  1. 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 Inf., 2015. report on NII website 4.2
  2. 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) 1.1
  3. 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) 3.1
  4. 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. 3.4
  5. 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: Scopus: 2-s2.0-84952056543) 3.1
  6. 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) 3.1
  7. 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) 3.1
  8. 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) 1.1
  9. 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) 3.1
  10. 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 4.2
  11. 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) 1.1
  12. 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) 3.1

Publications 2016

  1. D. Ahman, N. Ghani, G. Plotkin. Dependent types and fibred computational effects. 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. 36-54. Springer, 2016. doi: 10.1007/978-3-662-49630-5_3 (WOS: 000401936500003, Scopus: 2-s2.0-84961692317) 3.1
  2. 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 (WOS: 000390278400006, Scopus: 2-s2.0-84991629033) 3.1.
  3. S. Capobianco, J. Kari, S. Taati. An "almost dual" to Gottschalk's conjecture. In M. Cook, T. Neary, eds., Proc. of 22nd IFIP WG 1.5 Int. Wksh. on Cellular Automata and Discrete Complex Systems, AUTOMATA 2016 (Zurich, June 2016), v. 9664 of Lect. Notes in Comput. Sci., pp. 77-89. Springer, 2016. doi: 10.1007/978-3-319-39300-1_7 (WOS: 000389798900007, Scopus: 2-s2.0-84979021721) 3.1
  4. 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 (WOS: 000401936500006, Scopus: 2-s2.0-84961761094) 3.1
  5. A. Dieumegard, A. Toom, M. Pantel. Block library driven translation validation for dataflow models in safety critical systems. In M. H. ter Beek, S. Gnesi, A. Knapp, eds., Proc. of Joint 21st Int. Wksh. on Formal Methods for Industrial Critical Systems and 16th Int. Wksh. on Automated Verification of Critical Systems, FMICS-AVoCS 2016 (Pisa, Sept. 2016), v. 9933 of Lect. Notes in Comput. Sci., pp. 117-132. Springer, 2016. doi: 10.1007/978-3-319-45943-1_8 (WOS: 000389230800008, Scopus: 2-s2.0-84990061196) 3.1
  6. D. Firsov. Certification of Context-Free Grammar Algorithms, Thesis in Informatics and System Engineering C116, 118 pp. Tallinn Univ. of Techn., 2016. thesis in TUT DL 2.3
  7. D. Firsov, W. Jeltsch. Purely functional incremental computing. In F. Castor, Y. D. Liu, eds., Proc. of 20th Brazilian Symp. on Programming Languages, SBLP 2016 (Maringá, PR, Sept. 2016), v. 9889 of Lect. Notes in Comput. Sci., pp. 62-77. Springer, 2016. doi: 10.1007/978-3-319-45279-1_5 (Scopus: 2-s2.0-84989313938) 3.1
  8. 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 (WOS: 000390278400005, Scopus: 2-s2.0-84991672233) 3.1.
  9. M. Gaboardi, S.-y. Katsumata, D. Orchard, F. Breuvart, T. Uustalu. Combining effects and coeffects via grading. In Proc. of 21st ACM SIGPLAN Int. Conf. on Functional Programming, ICFP '16 (Nara, Sept. 2016), pp. 476-489. ACM Press, 2016. doi: 10.1145/2951913.2951939 3.1
  10. M. Gaboardi, S.-y. Katsumata, D. Orchard, F. Breuvart, T. Uustalu. Combining effects and coeffects via grading. ACM SIGPLAN Notices, v. 51, n. 9, pp. 476-489, 2016. doi: 10.1145/3022670.2951939 (WOS: 000393580700039) 1.1
  11. W. Jeltsch. Abstract categorical semantics for resourceful functional reactive programming. J. of Log. and Algebraic Methods in Program., v. 85, n. 6, pp. 1177-1200, 2016. doi: 10.1016/j.jlamp.2016.07.001 (WOS: 000388062000005, Scopus: 2-s2.0-84979619802) 1.1
  12. 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 4.1
  13. S. T. Taft, E. Richa, A. Toom. Building trust in a model-based automatic code generator. ACM SIGAda Ada Lett., v. 36, n. 2, pp. 54-57, 2016. doi: 10.1145/3092893.3092903 1.2
  14. H. Tamm. New interpretation and generalization of the Kameda-Weiner method. In I. Chatzigiannakis, M. Mitzenmacher, Y. Rabani, D. Sangiorgi, eds., Proc. of 43rd Int. Coll. on Automata, Languages and Programming, ICALP 2016 (Rome, July 2016), v. 55 of Leibniz Int. Proc. in Inf., article 116. Dagstuhl Publishing, 2016. doi: 10.4230/lipics.icalp.2016.116 (Scopus: 2-s2.0-85012877964) 3.1
  15. 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 (WOS: 000384382000018, Scopus: 2-s2.0-84978390183) 1.1
  16. T. Uustalu, J. Vain, guest eds. J. of Log. and Algebraic 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 (WOS:000388062000001, Scopus: 2-s2.0-85021667822) 4.1

Publications 2017

  1. D. Ahman, C. Hritcu, K. Maillard, G. Martínez, G. Plotkin, J. Protzenko, A. Rastogi, N. Swamy. Dijkstra monads for free. In Proc. of 44th ACM SIGPLAN Symp. on Principles of Programming Languages, POPL '17 (Paris, Jan. 2017), pp. 515-529. ACM Press, 2017. doi: 10.1145/3009837.3009878 (Scopus: 2-s2.0-85015310389) 3.1
  2. D. Ahman, C. Hritcu, K. Maillard, G. Martínez, G. Plotkin, J. Protzenko, A. Rastogi, N. Swamy. Dijkstra monads for free. ACM SIGPLAN Not., v. 52, n. 1, pp. 515-529, 2017. doi: 10.1145/3093333.3009878 (WOS: 000401538900037) 1.1
  3. D. Ahman, T. Uustalu. Taking updates seriously. In R. Eramo, M. Johnson, eds., Proc. of 6th Int. Wksh. on Bidirectional Transformations, BX 2017 (Uppsala, Apr. 2017), v. 1827 of CEUR Wksh. Proc., pp. 59-73. RWTH Aachen, 2017. article on publisher's website (Scopus: 2-s2.0-85019214713) 3.1
  4. S. Capobianco, J. Kari, S. Taati. Post-surjectivity and balancedness of cellular automata over groups. Discr. Math. and Theor. Comput. Sci., v. 19, n. 3, article 4, 2017. article in Episciences 1.1
  5. J. Chapman, T. Uustalu, N. Veltri. Formalizing rectriction categories. J. of Formaliz. Reason., v. 10, n. 1, pp. 1-36, 2017. doi: 10.6092/issn.1972-5787/6237 (WOS: 000406537100001) 1.1
  6. J. Chapman, T. Uustalu, N. Veltri. Quotienting the delay monad by weak bisimilarity. Math. Struct. in Comput. Sci., to appear. doi: 10.1017/s0960129517000184 (Scopus: 2-s2.0-85032199059) 1.1
  7. H. Maarand, T. Uustalu. Generating representative executions. 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 (WOS: 000405454500007, Scopus: 2-s2.0-85019247773) 3.1
  8. L. Pinto, T. Uustalu. A proof theoretic-study of bi-intuitionistic propositional sequent calculus. J. of Log. and Comput., to appear. 1.1
  9. H. Tamm, B. van der Merwe. Lower bound methods for the size of nondeterministic finite automata revisited. In F. Drewes, C. Martin-Vide, B. Truthe, eds., Proc. of 11th Int. Conf. on Language and Automata Theory and Applications, LATA 2017 (Umeå, March 2017), v. 10168 of Lect. Notes in Comput. Sci., pp. 261-272. Springer, 2017. doi: 10.1007/978-3-319-53733-7_19 (Scopus: 2-s2.0-85013378430) 3.1
  10. H. Tamm, M. Veanes. Theoretical aspects of symbolic automata. In Proc. of 44th Int. Conf. on Current Trends in Theory and Practice of Computer Science, SOFSEM 2018 (Krems an der Donau, Jan./Feb. 2018), Lect. Notes in Comput. Sci., Springer, to appear. 3.1
  11. 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 (Scopus: 2-s2.0-85032485332) 3.1
  12. T. Uustalu, ed. Proc. of 21st Int. Conf. on Types for Proofs and Programs, TYPES 2015 (Tallinn, May 2015), v. 69 of Leibniz Int. Proc. in Inf., Dagstuhl Publishing, in preparation. 4.1
  13. T. Uustalu, N. Veltri. Finiteness and rational sequences, constructively. J. of Funct. Program., v. 27, article e13, 2017. doi: 10.1017/s0956796817000041 (WOS: 000398525100001, Scopus: 2-s2.0-85017172351) 1.1
  14. 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., Springer, to appear. doi: 10.1007/978-3-319-71237-6_20 3.1
  15. 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 (Scopus: 2-s2.0-85031432824) 3.1
  16. N. Veltri. A Type-Theoretical Study of Nontermination, Thesis in Informatics and System Engineering C123, 143 pp. Tallinn Univ. of Techn., 2017. thesis in TUT DL 2.3

Tarmo Uustalu
Last update 6 November 2017