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. Electron. Notes in Theor. Comput. Sci., v. 82, n. 1 (H. P. Gumm, ed., Proc. of 6th Int. Wksh. on Coalgebraic Methods in Computer Science, CMCS '03, Warsaw, Apr. 2003), pp. 191-205, 2003. doi:10.1016/s1571-0661(04)80639-x (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. Electron. Notes in Theor. Comput. Sci., v. 106 (J. Adámek, S. Milius, eds., Proc. of 7th Int. Wksh. on Coalgebraic Methods in Computer Science, CMCS '04, Barcelona, March 2004), pp. 43-61, 2004. doi:10.1016/j.entcs.2004.02.034 (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. Electron. Notes in Theor. Comput. Sci. , v. 151, n. 3 (N. Thomas, ed., Proc. of 2nd Int. Wksh. on Practical Applications of Stochastic Modelling, PASM '05, Newcastle upon Tyne, July 2005), pp. 27-45. 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 ScienceOpen 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. Electron. Notes in Theor. Comput. Sci., v. 156, n. 1 (P. D. Mosses, I. Ulidowski, eds., Proc. of 2nd Wksh. on Structured Operational Semantics, SOS 2005, Lisbon, July 2005), pp. 151-168, 2006. doi:10.1016/j.entcs.2005.09.031 (WOS: 000214176700009, 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. Electron. Notes in Theor. Comput. Sci., v. 190, n. 1 (M. Huisman, F. Spoto, eds., Proc. of 2nd Wksh. on Bytecode Semantics, Verification, Analysis and Transformation, Bytecode 2007, Braga, March 2007), pp. 103-119, 2007. doi:10.1016/j.entcs.2007.02.063 (WOS: 000214246700008, 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 attributes 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 in HAL 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. doi:10.23658/taltech.nwpt/2008 4.2
  7. T. Uustalu, V. Vene. Comonadic notions of computation. Electron. Notes in Theor. Comput. Sci., v. 203, n. 5 (J. Adámek, C. Kupke, eds., Proc. of 9th Int. Wksh. on Coalgebraic Methods in Comput. Sci., CMCS 2008, Budapest, March 2008), pp. 263-284, 2008. doi:10.1016/j.entcs.2008.05.029 (WOS: 000214292900014, 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. doi:10.23658/taltech.fics/2009 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-85052024804) 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 (WOS: 000219473300006, 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 (WOS: 000219670000015, 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 (WOS: 000219536900007, Scopus: 2-s2.0-84954454791) 3.1
  11. T. Uustalu, V. Vene. The recursion scheme from the cofree recursive comonad. Electron. Notes in Theor. Comput. Sci., v. 229, n. 5 (V. Capretta, C. McBride, eds., Proc. of 2nd Wksh. on Mathematically Structured Functional Programming, MSFP 2008, Reykjavík, July 2008), pp. 135-157, 2011. doi:10.1016/j.entcs.2011.02.020 (WOS: 000216905700009, 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. D. Ahman, M. Kääramees. Constraint-based heuristic on-lin test generation from non-deterministic I/O EFSMs. In A. K. Petrenko, H. Schlingloff, eds., Proc. of 7th Wksh. on Model-Based Testing, MBT 2012 (Tallinn, March 2012), v. 80 of Electron. Proc. in Theor. Comput. Sci., pp. 115-129. Open Publishing Assoc., 2012. doi:10.4204/eptcs.80.9 (WOS:000219690400010, Scopus: 2-s2.0-84959354689) 3.1
  3. 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) 3.1
  4. 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
  5. 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
  6. 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) 3.1
  7. 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
  8. 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 (WOS: 000219685700001, Scopus: 2-s2.0-84958726191) 4.1
  9. 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
  10. W. Jeltsch. Towards a common categorical semantics for linear-time temporal logic and functional reactive programming. Electron. Notes in Theor. Comput. Sci., v. 286 (U. Berger, M. Mislove, eds., Proc. of 28th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXVIII, Bath, June 2012), pp. 229-242, 2012. doi:10.1016/j.entcs.2012.08.015 (WOS: 000216917900016, Scopus: 2-s2.0-84873472699) 1.1
  11. 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) 3.1
  12. 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 (WOS: 000219687100009, Scopus: 2-s2.0-84954560593) 3.1
  13. 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) 3.1

Publications 2013

  1. D. Ahman, S. Staton. Normalization by evaluation and algebraic effects. Electron. Notes in Theor. Comput. Sci., v. 298 (D. Kozen, M. Mislove, eds., Proc. of 29th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXIX, New Orleans, LA, June 2013), pp. 51-69, 2013. doi:10.1016/j.entcs.2013.09.007 (WOS: 000216920100005, 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 on 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 (WOS: 000440498800007, 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 (WOS: 000440497900007, 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 (WOS: 000219945800007, 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. doi:10.23658/taltech.nwpt/2013 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 (WOS: 000420001800004, 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. Electron. Notes in Theor. Comput. Sci., v. 308 (B. Jacobs, A. Silva, S. Staton, eds., Proc. of 30th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXX, Ithaca, NY, June 2014), pp. 25-48, 2014. doi:10.1016/j.entcs.2014.10.003 (WOS:000216920300003, 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 (WOS: 000219918500001, 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 (WOS: 000455397600025, 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 (WOS: 000420001800008, 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 (WOS: 000420001800005, 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 (WOS: 000491863900019, 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. doi: 10.23658/taltech.types/2015 4.2
  11. T. Uustalu. Stateful runners for effectful computations. Electron. Notes in Theor. Comput. Sci, v. 319 (D. Ghica, ed., Proc. of 31st Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXI, Nijmegen, June 2015), pp. 403-421, 2015. doi:10.1016/j.entcs.2015.12.024 (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 (WOS: 000448734800005, 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. 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 (WOS: 000455933500039, Scopus: 2-s2.0-85053066137) 3.1
  10. M. Gaboardi, S. 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. Fibred Computational Effects, PhD thesis, Lab. for Foundations of Comput. Sci., xi+452 pp. Univ. of Edinburgh, 2017. thesis in ERA 2.3
  2. 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
  3. 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, Scopus: 2-s2.0-85119348597) 1.1
  4. 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
  5. 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. doi:10.23638/dmtcs-19-3-4 (WOS: 00423286200005, Scopus: 2-s2.0-85032037915) 1.1
  6. J. Chapman, T. Uustalu, N. Veltri. Formalizing restriction categories. J. of Formaliz. Reason., v. 10, n. 1, pp. 1-36, 2017. doi:10.6092/issn.1972-5787/6237 (WOS: 000406537100001, Scopus: 2-s2.0-85037556982) 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. 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 (WOS: 000418579700019, Scopus: 2-s2.0-85013378430) 3.1
  9. 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 (WOS: 000449994500008, Scopus: 2-s2.0-85032485332) 3.1
  10. 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
  11. T. Uustalu, N. Veltri. Partiality and container monads. In B.-Y. E. Chang, ed., Proc. of 15th Asian Symp. on Programming Languages and Systems, APLAS 2017 (Suzhou, Nov. 2017), v. 10695 of Lect. Notes in Comput. Sci., pp. 406-425. Springer, 2017. doi:10.1007/978-3-319-71237-6_20 (WOS: 000611567400020, Scopus: 2-s2.0-85035057965) 3.1
  12. 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 (WOS: 000516829800003, Scopus: 2-s2.0-85031432824) 3.1
  13. 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

Publications 2018

  1. D. Ahman. Handling fibred algebraic effects. Proc. of ACM on Program. Lang., v. 2, n. POPL, article 7, 2018. doi:10.1145/3158095 (WOS: 000688016900007, Scopus: 2-s2.0-85120102531) 1.1
  2. D. Ahman. C. Fournet, C. Hritcu, K. Maillard, A. Rastogi, N. Swami. Recalling a witness: foundations and applications of monotonic state. Proc. of ACM on Program. Lang., v. 2, n. POPL, article 65, 2018. doi:10.1145/3158153 (WOS: 000688016900065, Scopus: 2-s2.0-85120135495) 1.1
  3. M. Bezem, T. Coquand, K. Nakata, E. Parmann. Realizability at work: separating two constructive notions of finiteness. In S. Ghilezan, H. Geuvers, J. Ivetic, eds., Proc. of 22nd Int. Conf. on Types for Proofs and Programs, TYPES '16 (Novi Sad, May 2016), v. 97 of Leibniz Int. Proc. in Inf., article 6. Dagstuhl Publishing, 2018. doi:10.4230/lipics.types.2016.6 (Scopus: 2-s2.0-85057046346) 3.1
  4. L. Diehl, D. Firsov, A. Stump. Generic zero-cost reuse for dependent types. Proc. of ACM on Program. Lang., v. 2, n. ICFP, article 104, 2018. doi:10.1145/3236799 (WOS: 000461309200038, WOS: 000688018100038, Scopus: 2-s2.0-85120117620) 1.1
  5. D. Firsov, R. Blair, A. Stump. Efficient Mendler-style lambda-encodings in Cedille. In J. Avigad, A. Mahboubi, eds., Proc. of 9th Int. Conf. on Interactive Theorem Proving, ITP 2018 (Oxford, July 2018), v. 10895 of Lect. Notes in Comput. Sci., pp. 235-252. Springer, 2018. doi:10.1007/978-3-319-94821-8_14 (WOS: 000490904100014, Scopus: 2-s2.0-85049895072) 3.1
  6. D. Firsov, A. Stump. Generic derivation of induction for impredicative encodings in Cedille. In Proc. of 7th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs, CPP 2018 (Los Angeles, CA, Jan. 2018), pp. 215-227. ACM, 2018. doi:10.1145/3167087 (Scopus: 2-s2.0-85044331588) 3.1
  7. B. Fischer, T. Uustalu, eds. Proc. of 15th Int. Coll. on Theoretical Aspects of Computer Science, ICTAC 2018 (Stellenbosch, Oct. 2018), v. 11187 of Lect. Notes in Comput. Sci., xvii+533 pp. Springer, 2018. doi:10.1007/978-3-030-02508-3 (Scopus: 2-s2.0-85055428657) 4.1
  8. S. Katsumata, T. Sato, T. Uustalu. Codensity lifting of monads and its dual. Log. Methods in Comput. Sci., v. 14, n. 4, article 6, 2018. doi:10.23638/lmcs-14(4:6)2018 (WOS: 000393580700039, Scopus: 2-s2.0-85060190543) 1.1
  9. H. Maarand, T. Uustalu. Certified Foata normalization for generalized traces. In A. Dutle, C. Muńoz, A. Narkawicz, eds., Proc. of 10th NASA Formal Methods Symp., NFM 2018 (Newport News, VA, Apr. 2018), v. 10811 of Lect. Notes in Comput. Sci., pp. 299-314. Springer, 2018. doi:10.1007/978-3-319-77935-5_21 (WOS: 000518166700021, Scopus: 2-s2.0-85045305218) 3.1
  10. L. Pinto, T. Uustalu. A proof theoretic-study of bi-intuitionistic propositional sequent calculus. J. of Log. and Comput., v. 28, n. 1, pp. 165-202, 2018. doi:10.1093/logcom/exx044 (WOS: 000454114000001, Scopus: 2-s2.0-85052635835) 1.1
  11. H. Tamm, M. Veanes. Theoretical aspects of symbolic automata. In A. M. Tjoa, L. Bellatreche, S. Biffl, J. van Leeuwen, J. Wiedermann, eds., Proc. of 44th Int. Conf. on Current Trends in Theory and Practice of Computer Science, SOFSEM 2018 (Krems an der Donau, Jan./Feb. 2018), v. 10706 of Lect. Notes in Comput. Sci., pp. 428-441. Springer, 2018. doi:10.1007/978-3-319-73117-9_30 (WOS: 000542576400030, Scopus: 2-s2.0-85041831906) 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., xii+250 pp. Dagstuhl Publishing, 2018. doi:10.4230/lipics.types.2015.0 (Scopus: 2-s2.0-85045435896) 4.1
  13. T. Uustalu, N. Veltri, N. Zeilberger. The sequent calculus of skew-monoidal categories. Electron. Notes in Theor. Comput. Sci., v. 341 (S. Staton, ed., Proc. of 34th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXIV, Halifax, NS, June 2018), pp. 345-370, 2018. doi:10.1016/j.entcs.2018.11.017 (WOS: 000452898800017, Scopus: 2-s2.0-85058062732) 1.1

Publications 2019

  1. D. Ahman, T. Uustalu. Decomposing comonad morphisms. In M. Roggenbach, A. Sokolova, eds., Proc. of 8th Conf. on Algebra and Coalgebra in Computer Science, CALCO 2019 (London, June 2019), v. 139 of Leibniz Int. Proc. in Inf., art. 14, 19 pp. Dagstuhl Publishing, 2019. doi:10.4230/lipics.calco.2019.14 (Scopus: 2-s2.0-85076039926) 3.1.
  2. A. Buldas, D. Firsov, R. Laanoja, H. Lakk, A. Truu. A new approach to constructing digital signature schemes. In N. Attrapadung, T. Yagi, eds., Proc. of 14th Int. Wksh. on Security, IWSEC 2019 (Tokyo, Aug. 2019), v. 11689 of Lect. Notes in Comput. Sci., pp. 363-373. Springer, 2019. doi:10.1007/978-3-030-26834-3_21 (WOS: 000612998800021, Scopus: 2-s2.0-85071436047) 3.1
  3. J. Chapman, T. Uustalu, N. Veltri. Quotienting the delay monad by weak bisimilarity. Math. Struct. in Comput. Sci., v. 29, n. 1, pp. 67-92, 2019. doi:10.1017/s0960129517000184 (WOS: 000451889100004, Scopus: 2-s2.0-85032199059) 1.1
  4. J. Espírito Santo, L. Pinto, T. Uustalu. Modal embeddings and calling paradigms. In H. Geuvers, ed., Proc. of 4th Int. Conf. on Formal Structures for Computation and Deduction, FSCD 2019 (Dortmund, June 2019), v. 131 of Leibniz Int. Proc. in Inf., art. 18, 20 pp. Dagstuhl Publishing, 2019. doi:10.4230/lipics.fscd.2019.18 (Scopus: 2-s2.0-85068045398) 3.1.
  5. R. Kaarsgaard, N. Veltri. En garde! Unguarded iteration for reversible computation in the delay monad. In G. Hutton, ed., Proc. of 13th Int. Conf. on Mathematics of Program Construction, MPC 2019 (Porto, Oct. 2019), v. 11825 of Lect. Notes in Comput. Sci., pp. 366-384. Springer, 2019. doi:10.1007/978-3-030-33636-3_13 (WOS: 000716932700013, Scopus: 2-s2.0-85076114425) 3.1
  6. H. Maarand, T. Uustalu. Certified normalization of generalized traces. Innov. in Syst. and Softw. Engin., v. 15, n. 3-4, pp. 253-265, 2019. doi:10.1007/s11334-019-00347-1 (WOS: 000482389700006, Scopus: 2-s2.0-85067808291) 1.1
  7. H. Maarand, T. Uustalu. Reordering derivatives of trace closures of regular languages. In W. Fokkink, R. van Glabbeek, eds., Proc. of 30th Int. Conf. on Concurrency Theory, CONCUR 2019 (Amsterdam, Aug. 2019), v. 140 of Leibniz. Int. Proc. in Inf., art. 40, 16 pp. Dagstuhl Publishing, 2019. doi:10.4230/lipics.concur.2019.40 (Scopus: 2-s2.0-85071609227) 3.1
  8. K. Maillard, D. Ahman, R. Atkey, G. Martínez, C. Hritcu, E. Rivas, É. Tanter. Dijkstra monads for all. Proc. of ACM on Program. Lang., v. 3, n. ICFP, art. 104, 29 pp., 2019. doi:10.1145/3341708 (WOS: 000685201900027, Scopus: 2-s2.0-85120102650) 1.1
  9. G. Martínez, D. Ahman, V. Dumitrescu, N. Giannarakis, C. Hawblitzel, C. Hritcu, M. Narasimhamurthy, Z. Paraskevopoulou, C. Pit-Claudel, J. Protzenko, T. Ramananandro, A. Rastogi, N. Swamy. Meta-F*: proof automation with SMT, tactics, and metaprograms. In L. Caires, ed., Proc. of 28th Europ. Symp. on Programming, ESOP 2019 (Prague, Apr. 2019), v. 11423 of Lect. Notes in Comput. Sci., pp. 30-59. Springer, 2019. doi:10.1007/978-3-030-17184-1_2 (WOS: 000681669300002, Scopus: 2-s2.0-85064919038) 3.1
  10. R. E. Mřgelberg, N. Veltri. Bisimulation as path type for guarded recursive types. Proc. of ACM on Program. Lang., v. 3, n. POPL, art. 4, 29 pp., 2019. doi:10.1145/3290317 (WOS: 000678450300004, Scopus: 2-s2.0-85079466275) 1.1
  11. T. Uustalu, J. Vain, eds. Abstracts of 31st Nordic Wksh. on Programming Theory, NWPT 2019 (Tallinn, Nov. 2019), vii+88 pp. Tallinn Univ. of Techn., 2019. doi:10.23658/taltech.nwpt/2019 4.2
  12. N. Veltri, N. van der Weide. Guarded recursion in Agda via sized types. In H. Geuvers, ed., Proc. of 4th Int. Conf. on Formal Structures for Computation and Deduction, FSCD 2019 (Dortmund, June 2019), v. 131 of Leibniz Int. Proc. in Inf., art. 32, 19 pp. Dagstuhl Publishing, 2019. doi:10.4230/lipics.fscd.2019.32 (Scopus: 2-s2.0-85068029461) 3.1.

Publications 2020

  1. D. Ahman, A. Bauer. Runners in action. In P. Müller, ed., Proc. of 29th Europ. Symp. on Programming, ESOP 2020 (Dublin, Apr. 2020), v. 12075 of Lect. Notes in Comput. Sci., pp. 29-55. Springer, 2020. doi:10.1007/978-3-030-44914-8_2 (WOS: 000681656800002, Scopus: 2-s2.0-85083973354) 3.1
  2. S. Capobianco, P. Guillon. A characterization of amenable groups with Besicovitch pseudodistances. In H. Zenil, ed., Proc. of 26th IFIP WG 1.5 Int. Wksh. on Cellular Automata and Discrete Complex Systems, AUTOMATA 2020 (Stockholm, Aug. 2020), v. 12286 of Lect. Notes in Comput. Sci., pp. 99-110. Springer, 2020. doi:10.1007/978-3-030-61588-8_8 (Scopus: 2-s2.0-85096516802) 3.1
  3. D. Firsov, A. Buldas, A. Truu, R. Laanoja. Verified security of BLT signature scheme. In Proc. of 9th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs, CPP 2020 (New Orleans, LA, Jan. 2020), pp. 244-257. ACM Press, 2020. doi:10.1145/3372885.3373828 (WOS: 000620147900020, Scopus: 2-s2.0-85079442346) 3.1
  4. S. Katsumata, E. Rivas, T. Uustalu. Interaction laws of monads and comonads. In Proc. of 35th Ann. ACM/IEEE Symp. on Logic in Computer Science, LICS 2020 (Saarbrücken, July 2020), pp. 604-618. ACM Press, 2020. doi:10.1145/3373718.3394808 (WOS: 000665014900047, Scopus: 2-s2.0-85085952830) 3.1
  5. H. Maarand. Operational Semantics of Weak Sequential Composition, Doctoral Thesis 17/2020, 146 pp. Tallinn Univ. of Technology, 2020. doi:10.23658/taltech.17/2020 2.3
  6. B. Mannaa, R. E. Mřgelberg, N. Veltri. Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory. Log. Methods Comput. Sci., v. 16, n. 4, art. 17, 31 pp., 2020. doi:10.23638/lmcs-16(4:17)2020 (WOS: 000605983500019, Scopus: 2-s2.0-85101631804) 1.1
  7. D. McDermott, M. Piróg, T. Uustalu. Degrading lists. In Proc. of 22nd Int. Symp. on Principles and Practice of Declarative Languages, PPDP 2020 (Bologna, Sept. 2020), ACM Int. Conf. Proc. Series, article 6, 14 pp. ACM Press, 2020. doi:10.1145/3414080.3414084 (Scopus: 2-s2.0-85092799037) 3.1
  8. N. Swamy, A. Rastogi, A. Fromherz, D. Merigoux, D. Ahman, G. Martínez. SteelCore: an extensible concurrent separation logic for effectful dependently typed programs. Proc. of ACM on Program. Lang., v. 4, n. ICFP, article 121, 30 pp., 2020. doi:10.1145/3409003 (WOS: 000685203700035, Scopus: 2-s2.0-85090268357) 1.1
  9. H. Tamm. Quotients and atoms of reversible languages. In E. Sekerinski, N. Moreira et al., eds., Revised Selected Papers from FM 2019 Int. Wkshs. (Porto, Oct. 2019), Part II, v. 12233 of Lect. Notes in Comput. Sci., pp. 443-455. Springer, 2020. doi:10.1007/978-3-030-54997-8_28 (Scopus: 2-s2.0-85089715772) 3.1
  10. T. Uustalu, N. Veltri, N. Zeilberger. Eilenberg-Kelly reloaded. Electron. Notes in Theor. Comput. Sci., v. 352 (P. Johann, ed., Proc. of 36th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXVI, Paris, June 2020), pp. 233-256, 2020. doi:10.1016/j.entcs.2020.09.012 (WOS: 000582228200012, Scopus: 2-s2.0-85101225913) 1.1
  11. T. Uustalu, N. Voorneveld. Algebraic and coalgebraic perspectives on interaction laws. In B. C. d. S. Oliveira, ed., Proc. of 18th Asian Symp. on Programming Languages and Systems, APLAS 2020 (Fukuoka, Nov./Dec. 2020), v. 12470 of Lect. Notes in Comput. Sci., pp. 186-205. Springer, 2020. doi:10.1007/978-3-030-64437-6_10 (WOS: 000916297300010, Scopus: 2-s2.0-85097654344) 3.1
  12. N. Veltri, A. Vezzosi. Formalizing π-calculus in guarded cubical Agda. In Proc. of 9th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs, CPP 2020 (New Orleans, LA, Jan. 2020), pp. 270-283. ACM Press, 2020. doi:10.1145/3372885.3373814 (WOS: 000620147900022, Scopus: 2-s2.0-85079443514) 3.1
  13. N. Voorneveld. Combining algebraic effect descriptions using the tensor of complete lattices. Electron. Notes in Theor. Comput. Sci., v. 352 (P. Johann, ed., Proc. of 36th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXVI, Paris, June 2020), pp. 257-281, 2020. doi:10.1016/j.entcs.2020.09.013 (WOS: 000582228200013, Scopus: 2-s2.0-85114396355) 1.1
  14. N. Voorneveld. From equations to distinctions: two interpretations of effectful computations. In M. S. New, S. Lindley, eds., Proc. of 8th Wksh. on Mathematically Structured Functional Programming, MSFP 2020 (Dublin, Apr. 2020), v. 317 of Electron. Proc. in Theor. Comput. Sci., pp. 1-17. Open Publ. Assoc., 2020. doi:10.4204/eptcs.317.1 (Scopus: 2-s2.0-85085695615) 3.1

Publications 2021

  1. B. Ahrens, D. Frumin, M. Maggesi, N. Veltri, N. van der Weide. Bicategories in Univalent Foundations. Math. Struct. Comput. Sci., v. 31, n. 10, pp. 1232-1269, 2021. doi:10.1017/s0960129522000032 (WOS: 000767071800001, Scopus: 2-s2.0-85126564877) 1.1
  2. D. Ahman, M. Pretnar. Asynchronous effects. Proc. of ACM on Program. Lang., v. 5, n. POPL, art. 24, 28 pp., 2021. doi:10.1145/3434305 (WOS: 000679806100024, Scopus: 2-s2.0-85099030255) 1.1
  3. S. Capobianco, P. Guillon. Besicovitch pseudodistances with respect to non-Fřlner sequences. Complex Syst., v. 30, n. 2, pp. 133-158, 2021. doi:10.25088/complexsystems.30.2.133 (WOS: 000657100700002, Scopus: 2-s2.0-85108285187) 1.1
  4. D. Firsov, H. Lakk, S. Laur, A. Truu. BLT+L: efficient signatures from timestamping and endorsements. In S. De Capitani di Vimercati, P. Samarati, eds., Proc. of 18th Int. Conf. on Security and Cryptography, SECRYPT 2021 (Milan, July 2021), pp. 75-86. SciTePress, 2021. doi: 10.5220/0010530000750086 (WOS: 000720102500006, Scopus: 2-s2.0-85111808694) 3.1
  5. D. Firsov, H. Lakk, A. Truu. Verified multiple-time signature scheme from one-time signatures and timestamping. In Proc. of 34th IEEE Computer Security Foundations Symp., CSF 2021 (Dubrovnik, June 2021), pp. 653-665. IEEE, 2021. doi:10.1109/csf51468.2021.00051 (WOS: 000719322000041, Scopus: 2-s2.0-85124030778) 3.1
  6. H. Maarand, T. Uustalu. Operational semantics with semicommutations. J. of Log. and Algebraic Methods in Program., v. 121, art. 100677, 27 pp., 2021. doi:10.1016/j.jlamp.2021.100677 (WOS: 000653017200003, Scopus: 2-s2.0-85104417236) 1.1
  7. H. Tamm. Boolean automata and atoms of regular languages. In F. Bonchi, S. J. Puglisi, eds., Proc. of 46th Int. Symp. on Mathematical Foundations of Computer Science, MFCS 2021 (Tallinn, Estonia, Aug. 2021), v. 202 of Leibniz Int. Proc. in Inform., article 86, 13 pp. Dagstuhl Publishing, 2021. doi:10.4230/lipics.mfcs.2021.86 (Scopus: 2-s2.0-85115397554) 3.1
  8. T. Uustalu, N. Veltri, N. Zeilberger. Deductive systems and coherence for skew prounital closed categories. In C. Sacerdoti Coen, A. Tiu, eds., Proc. of 15th Int. Wksh. on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP 2020 (Paris, June 2020), v. 332 of Electron. Proc. in Theor. Comput. Sci., pp. 35-53. Open Publishing Assoc., 2021. doi:10.4204/eptcs.332.3 (Scopus: 2-s2.0-85101209607) 3.1
  9. T. Uustalu, N. Veltri, N. Zeilberger. Proof theory of partially normal skew monoidal categories. In D. I. Spivak, J. Vicary, eds., Proc. of 3rd Ann. Int. Applied Category Theory Conf., ACT 2020 (Cambridge, MA, July 2020), v. 333 of Electron. Proc. in Theor. Comput. Sci., pp. 230-246. Open Publishing Assoc., 2021. doi:10.4204/eptcs.333.16 (Scopus: 2-s2.0-85101268643) 3.1
  10. T. Uustalu, N. Veltri, N. Zeilberger. The sequent calculus of skew monoidal categories. In C. Casadio, P. J. Scott, eds., Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, v. 20 of Outstanding Contributions to Logic, pp. 377-406. Springer, 2021. doi:10.1007/978-3-030-66545-6_11 (Scopus: 2-s2.0-85103071845) 3.1
  11. N. Veltri. Coherence via focusing for symmetric skew monoidal categories. In A. Silva, R. Wassermann, R. de Queiroz, eds., Proc. of 27th Wksh. on Logic, Language, Information and Computation, WoLLIC 2021 (Oct. 2021), v. 13038 of Lect. Notes in Comput. Sci., pp. 184-200. Springer, 2021. doi:10.1007/978-3-030-88853-4_12 (WOS: 000876648000012, Scopus: 2-s2.0-85117482051) 3.1
  12. N. Veltri. Type-theoretic constructions of the final coalgebra of the finite powerset functor. In N. Kobayashi, ed., Proc. of 6th Int. Conf. on Formal Structures for Computation and Deduction, FSCD 2021 (Buenos Aires, July 2021), v. 195 of Leibniz Int. Proc. in Inform., art. 22, 18 pp. Dagstuhl Publishing, 2021. doi:10.4230/lipics.fscd.2021.22 (Scopus: 2-s2.0-85115213929) 3.1
  13. N. Veltri, N. Benton, S. Ghilezan, eds. Proc. of 23rd Int. Symp. on Principles and Practice of Declarative Programming, PPDP '21 (Tallinn, Sept. 2021), ACM Int. Conf. Proc. Series, vi pp.+23 articles. ACM Press, 2021. doi:10.1145/3479394 (Scopus: 2-s2.0-85117737338) 4.1
  14. N. Veltri, N. van der Weide. Constructing higher inductive types as groupoid quotients. Log. Methods Comput. Sci., v. 17, n. 2, art. 8, 42 pp., 2021. doi:10.23638/lmcs-16(2:8)2021 (WOS: 000658731000009, Scopus: 2-s2.0-85105276320) 1.1
  15. N. Veltri, N. Voorneveld. Inductive and coinductive predicate liftings for effectful programs. In A. Sokolova, ed., Proc. of 37th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXVII (Salzburg, Aug./Sept. 2021), v. 351 of Electron. Proc. in Theor. Comput. Sci., pp. 260-277. Open Publishing Assoc., 2021. doi:10.4204/eptcs.351.16 3.1 (Scopus: 2-s2.0-85122280172)

Publications 2022

  1. M. Bortin. Synthesis of implementations for divide-and-conquer specifications. In L. Lima, V. Molnár, eds., Proc. of 25th Brazilian Symp. on Formal Methods, SBMF 2022 (Dec. 2022), v. 13768 of Lect. Notes in Comput. Sci., Springer, pp. 73-88. Springer, 2022. doi:10.1007/978-3-031-22476-8_5 (WOS: 000922881500005, Scopus: 2-s2.0-85144302200) 3.1
  2. S. Capobianco. Fekete's lemma for componentwise subadditive functions of two or more real variables. Acta Comment. Math. Univ. Tartuensis, v. 26, n. 1, pp. 45-62, 2022. doi:10.12697/acutm.2022.26.04 (WOS: 000810997700004, Scopus: 2-s2.0-85133014553) 1.1
  3. J. Espírito Santo, L. Pinto, T. Uustalu. Plotkin's call-by-value λ-calculus as a modal calculus. J. of Log. and Algebraic Methods in Program., v. 127, art. 100775, 17 pp., 2022. doi:10.1016/j.jlamp.2022.100775 (WOS: 000799966300001, Scopus: 2-s2.0-85129234344) 1.1
  4. D. Firsov, D. Unruh. Reflection, rewinding and coin-toss in Easycrypt. In Proc. of 11th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs, CPP '22 (Philadelphia, PA, Jan. 2022), pp. 166-179. ACM Press, 2022. doi:10.1145/3497775.3503693 (WOS: 000926563600015, Scopus: 2-s2.0-85124031830) 3.1
  5. D. Firsov, S. Laur, E. Zhuchko. Unsatisfiability of comparison-based non-malleability for commitments. In H. Seidl, Z. Liu, C. S. Pasareanu, eds., Proc. of 19th Int. Coll. on Theoretical Aspects of Computing, ICTAC 2022 (Tbilisi, Sept. 2022), v. 13572 of Lect. Notes in Comput. Sci., pp. 188-194. Springer, 2022. doi:10.1007/978-3-031-17715-6_13 (Scopus: 2-s2.0-85140722547) 3.1
  6. H. Maarand, H. Tamm. Yet another canonical nondeterministic automaton. In Y.-S. Han, G. Vaszil, eds., Proc. of 24th IFIP WG 1.2 Int. Conf. on Descriptional Complexity of Formal Systems, DCFS 2022 (Debrecen, Aug. 2022), v. 13439 of Lect. Notes in Comput. Sci., pp. 184-196. Springer, 2022. doi:10.1007/978-3-031-13257-5_14 (WOS: 000877345300016, Scopus: 2-s2.0-85137043087) 3.1
  7. S. Katsumata, D. McDermott, T. Uustalu, N. Wu. Flexible presentations of graded monads. Proc. of ACM on Program. Lang., v. 6, n. ICFP, art. 123, 29 pp., 2022. doi:10.1145/3547654 (WOS: 000851562000034, Scopus: 2-s2.0-85139198557) 1.1
  8. D. McDermott, Y. Morita, T. Uustalu. A type system with subtyping for WebAssembly's stack polymorphism. In H. Seidl, Z. Liu, C. S. Pasareanu, eds., Proc. of 19th Int. Coll. on Theoretical Aspects of Computing, ICTAC 2022 (Tbilisi, Sept. 2022), v. 13572 of Lect. Notes in Comput. Sci., pp. 305-323. Springer, 2022. doi:10.1007/978-3-031-17715-6_20 (Scopus: 2-s2.0-85140780525) 3.1
  9. D. McDermott, E. Rivas, T. Uustalu. Sweedler theory of monads. In P. Bouyer, L. Schröder, eds., Proc. of 25th Int. Conf. on Software Science and Computation Structures, FoSSaCS 2022 (Munich, Apr. 2022), v. 13242 of Lect. Notes in Comput. Sci., pp. 428-448. Springer, 2022. doi:10.1007/978-3-030-99253-8_22 (WOS: 000782446800022, Scopus: 2-s2.0-85128459922) 3.1
  10. D. McDermott, T. Uustalu. Flexibly graded monads and graded algebras. In E. Komendantskaya, ed., Proc. of 14th Int. Conf. on Mathematics of Program Construction, MPC 2022 (Tbilisi, Sept. 2022), v. 13544 of Lect. Notes in Comput. Sci., pp. 102-128. Springer, 2022. doi:10.1007/978-3-031-16912-0_4 (WOS: 000866537100004, Scopus: 2-s2.0-85140428749) 3.1
  11. D. McDermott, T. Uustalu. What makes a strong monad? In J. Gibbons, M. S. New, eds., Proc. of 9th Wksh. on Mathematically Structured Functional Programming, MSFP 2022 (Munich, Apr. 2022), v. 360 of Electron Proc. in Theor. Comput. Sci., pp. 113-133. Open Publishing Assoc., 2022. doi:10.4204/eptcs.360.6 (Scopus: 2-s2.0-85134196437) 3.1
  12. H. Tamm. Quotients and atoms of reversible languages. Theor. Comput. Sci., v. 920, pp. 33-45, 2022. doi:10.1016/j.tcs.2022.02.023 (WOS: 000830247200004, Scopus: 2-s2.0-85125740252) 1.1
  13. T. Uustalu, N. Veltri, C.-S. Wan. Proof theory of skew non-commutative MILL. In A. Indrzejczak, M. Zawidzki, eds., Proc. of 10th Int. Conf. on Non-classical Logics: Theory and Applications, NCL '22 (Łódź, March 2022), v. 358 of Electron. Proc. in Theor. Comput. Sci., pp. 118-135. Open Publishing Assoc., 2022. doi:10.4204/eptcs.358.9 (Scopus: 2-s2.0-85130481250) 3.1
  14. N. Veltri. Normalization by evaluation for the Lambek calculus. In A. Indrzejczak, M. Zawidzki, eds., Proc. of 10th Int. Conf. on Non-classical Logics: Theory and Applications, NCL '22 (Łódź, March 2022), v. 358 of Electron. Proc. in Theor. Comput. Sci., pp. 102-117. Open Publishing Assoc., 2022. doi:10.4204/eptcs.358.8 (Scopus: 2-s2.0-85130481431) 3.1
  15. N. Veltri, N. Voorneveld. Streams of approximations, equivalence of recursive effectful programs. In E. Komendantskaya, ed., Proc. of 14th Int. Conf. on Mathematics of Program Construction, MPC 2022 (Tbilisi, Sept. 2022), v. 13544 of Lect. Notes in Comput. Sci., pp. 198-221. Springer, 2022. doi:10.1007/978-3-031-16912-0_8 (WOS: 000866537100008, Scopus: 2-s2.0-85140468970) 3.1
  16. N. Voorneveld. Runners for concurrent effectful programs. In H. Seidl, Z. Liu, C. S. Pasareanu, eds., Proc. of 19th Int. Coll. on Theoretical Aspects of Computing, ICTAC 2022 (Tbilisi, Sept. 2022), v. 13572 of Lect. Notes in Comput. Sci., pp. 407-424. Springer, 2022. doi:10.1007/978-3-031-17715-6_26 (Scopus: 2-s2.0-85140722139) 3.1

Publications 2023

  1. F. Breuvart, D. McDermott, T. Uustalu. Canonical gradings of monads. In M. Lewis, J. Master, eds., Proc. of 5th Int. Conf. on Applied Category Theory, ACT 2022 (Glasgow, July 2022), Electron. Proc. in Theor Comput. Sci., Open Publishing Assoc., to appear. article on publisher's website 3.1
  2. D. Firsov, D. Unruh. Zero-knowledge in Easycrypt. In Proc. of 36th IEEE Computer Security Foundations Symp., CSF 2023 (Dubrovnik, July 2023), IEEE, to appear. 3.1
  3. N. Veltri, A. Vezzosi. Formalizing CCS and π-calculus in guarded cubical Agda. J. Log. and Algebraic Methods in Comput., v. 131, art. 100846, 23 pp., 2023. doi:10.1016/j.jlamp.2022.100846 (Scopus: 2-s2.0-85146099127) 1.1
Tarmo Uustalu
Last update 13 March 2023