Tarmo Uustalu's publications

• 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), Electron. Notes in Theor. Comput. Sci., Elsevier, to appear.
• T. Uustalu. Coherence for skew-monoidal categories.
  In N. Krishnaswamy, 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 link - Agda code
• D. Ahman, T. Uustalu. Update monads: cointerpreting directed containers.
  In R. Matthes, A. Schubert, eds., Proc. of 19th Conf. on Types for Proofs and Programs, TYPES 2013 (Toulouse, Apr. 2013), v. 26 of Leibniz Int. Proc. in Inform, pp. 1-23. Dagstuhl Publishing, 2014. doi link - .pdf, 537K
• J. Chapman, T. Uustalu, N. Veltri. Formalizing restriction categories.
  Manuscript.
• D. Firsov, T. Uustalu. Certified CYK parsing of context-free languages.
  Submitted.
• 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 link - (© Springer)
• 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 link - Haskell code
• D. Ahman, T. Uustalu. Distributive laws of directed containers.
  Progress in Informatics, v. 10, pp. 3-18, 2013. doi link //
  Extended abstract in L. Schröder, D. Pattinson, eds., Short Contributions of 11th Int. Wksh. on Coalgebraic Methods in Comput. Sci., CMCS '12 (Tallinn, March/April 2012), pp. 1-3. Inst. of Cybernetics, 2012. - .pdf, 162K
• T. Uustalu. Structured general corecursion and coinductive graphs (extended abstract).
  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 link
• T. Uustalu. Explicit folds: 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 link - .pdf, 172K (© Springer)
• D. Ahman, J. Chapman, T. Uustalu. When is a container a comonad?
  Logical Methods in Comput. Sci., to appear. //
  Conf. version 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 link - .pdf, 268K (© Springer) - project page, incl. Agda code
• 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 link - .pdf, 270K (© Springer)
• M. Bezem, K. Nakata, T. Uustalu. On streams that are finitely red.
  Logical Methods in Comput. Sci., v. 8, n. 4, article 4, 2012. doi link
• 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. - .pdf, 230K
• 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 link - .pdf, 146K
• T. Uustalu. A note on strong dinaturality, initial algebras and uniform parameterized fixpoint operators (extended abstract).
  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. - .pdf, 130K
• 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 link - .pdf, 176K
• T. Uustalu. Strong relative monads (extended abstract).
  In B. Jacobs, M. Niqui, J. Rutten, A. Silva, eds., Short Contributions of 10th Int. Wksh. on Coalgebraic Methods in Comput. Sci., CMCS '10 (Paphos, March 2010), pp. 23-24. CWI, 2010.
• T. Altenkirch, J. Chapman, T. Uustalu. Relative monads formalised.
  J. of Formalized Reasoning, v. 7, n. 1, pp. 1-43, 2014. doi link - .pdf, 285K
• T. Altenkirch, J. Chapman, T. Uustalu. Monads need not be endofunctors.
  Logical Methods in Comput. Sci., to appear. //
  Conf. version 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 link - .pdf, 241K (© Springer)
• K. Nakata, T. Uustalu. A Hoare logic for the coinductive trace-based big-step semantics of While.
  Manuscript, 2010. //
  Conf. version 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 link - .pdf, 229K (© Springer)
• 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 link - .pdf, 245K (© Springer)
• 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 link - .pdf, 147K (© IEEE)
• 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 link - .pdf, 292K (© Springer)
• 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 link - free pdf from ACM DL (via ACM Author-Izer) (© ACM)
• 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 link - .pdf, 287K
• V. Capretta, T. Uustalu, V. Vene. Corecursive algebras: a study of general 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 link - .pdf, 296K (© Springer)
• A. Saabas, T. Uustalu. Proof optimization for partial redundancy elimination.
  J. of Logic and Algebr. Program., v. 78, n. 7, pp. 620-643, 2009. doi link - .pdf, 462K (accepted author manuscript, © Elsevier Science) //
  Conf. version 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 link - free pdf from ACM DL (via ACM Author-Izer) (© ACM)
• T. Uustalu, V. Vene. Comonadic notions of computation.
  In J. Adámek, C. Kupke, eds., Proc. of 9th Int. Wksh. on Coalgebraic Methods in Computer Science, CMCS 2008 (Budapest, Apr. 2008), v. 203, n. 5 of Electron. Notes in Theor. Comput. Sci., pp. 263-284. Elsevier, 2008. doi link - .pdf, 282K (accepted author manuscript, © Elsevier Science)
• 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 link - .pdf, 505K (© Springer)
• A. Saabas, T. Uustalu. Program and proof optimizations with type systems.
  J. of Logic and Algebr. Program., v. 77, n. 1-2, pp. 131-154, 2008. doi link - .pdf, 316K (accepted author manuscript, © Elsevier Science)
• M. J. Frade, A. Saabas, T. Uustalu. Foundational certification of data-flow analyses.
  In Proc. of 1st IEEE and IFIP Int. Symp on Theor. Aspects of Software Engineering, TASE 2007 (Shanghai, June 2007), pp. 107-116. IEEE CS Press, 2007. doi link - .pdf, 280K (© IEEE)
• 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 link - .pdf, 304K (accepted author manuscript, © Elsevier Science)
• 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. - .pdf, 72K
• A. Saabas, T. Uustalu. Compositional type systems for stack-based low-level languages.
  Manuscript. - .pdf, 402K //
  Conf. version in B. Jay, J. Gudmundsson, eds., Proc. of 12th Computing, Australasian Theory Symp., CATS 2006 (Hobart, Jan. 2006), v. 51 of Confs. in Research and Practice in Inform. Techn., pp. 27-39. Australian Comput. Soc., 2006. article in ACM DL - .pdf, 270K (© Australian Comput. Soc.)
• T. Uustalu, V. Vene. Comonadic functional attribute evaluation.
  In M. van Eekelen, ed., Trends in Functional Programming 6, pp. 145-162. Intellect, 2007. book in Google Books - .pdf, 67K //
  Conf. version 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.
• 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 link - .pdf, 260K (accepted author manuscript, © Elsevier Science) //
  Conf. version in M. Hofmann, H.-W. Loidl, eds., Proc. of 3rd APPSEM II Wksh., APPSEM '05 (Frauenchiemsee, Sept. 2005), 12 pp. Ludwig-Maximilians-Univ. München, 2005.
• 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 link - .pdf, 325K (accepted author manuscript, © Elsevier Science) //
  Conf. version in P. D Mosses, I. Ulidowski, eds., Proc. of 2nd Wksh. on Structured Operational Semantics, SOS '05 (Lisbon, July 2005), v. 156, n. 1 of Electron. Notes in Theor. Comput. Sci., pp. 151-168. Elsevier, 2006. doi link - .pdf, 269K (accepted author manuscript, © Elsevier Science)
• T. Uustalu, V. Vene. The essence of dataflow programming.
  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 link - .pdf, 497K (© Springer) //
  Short conf. 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 link - .pdf, 363K (© Springer)
• T. Uustalu, V. Vene. Signals and comonads.
  J. of Univ. Comput. Sci., v. 11, n. 7, pp. 1310-1326, 2005. doi link - .pdf, 135K (© J. of Univ. Comput. Sci.) //
  Conf. version 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.
• 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) (= ACM SIGPLAN Notices, v. 40, n. 9), pp. 294-305. ACM Press, 2005. doi link - free pdf from ACM DL (via ACM Author-Izer) (© ACM)
• 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. - .pdf, 74K
• 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 link - .pdf, 255K (© Springer)
• N. Ghani, T. Uustalu. Monad combinators, non-determinism and probabilistic choice (extended abstract).
  Manuscript, distributed at CMCIM 2004 (Copenhagen, Aug. 2004) - .pdf, 180K
• V. Capretta, T. Uustalu, V. Vene. Recursive coalgebras from comonads.
  Inform. and Comput., v. 204, n. 4, pp. 437-468, 2006. doi link - .pdf, 447K (accepted author manuscript, © Elsevier Science) //
  Conf. version 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 link - .pdf, 257K (accepted author manuscript, © Elsevier Science)
• 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 link - .pdf, 219K (© Springer)
• N. Ghani, T. Uustalu, M. Hamana. Explicit substitutions and higher-order syntax.
  Higher-Order and Symb. Comput., v. 19, n. 2-3, pp. 263-282, 2006. doi link - .pdf, 330K (© Springer) //
  Conf. version 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 link - free pdf from ACM DL (via ACM Author-Izer) (© ACM)
• N. Ghani, T. Uustalu. Coproducts of ideal monads.
  Theor. Inform. and Appl., v. 38, n. 4, pp. 321-342, 2004. doi link, article at NUMDAM - .pdf, 290K (© EDP Sciences) //
  Extended abstract in Z. Ésik, I. Walukiewicz, ed., Proc. of 5th Int. Wksh. on Fixed Points in Computer Science, FICS '03 (Warsaw, Apr. 2003), pp. 32-36. Warsaw Univ., 2003.
• T. Uustalu, V. Vene. An alternative characterization of complete iterativeness (extended abstract).
  In Z. Ésik, I. Walukiewicz, ed., Proc. of 5th Int. Wksh. on Fixed Points in Computer Science, FICS '03 (Warsaw, Apr. 2003), pp. 81-83. Warsaw Univ., 2003.
• 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 link - .pdf, 255K (accepted author manuscript, © Elsevier Science) //
  Conf. version 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.. Elsevier, 2003. doi link - .pdf, 305K
• 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 link - .pdf, 450K (accepted author manuscript, © Elsevier Science) //
  Conf. version 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 link - .pdf, 227K (© Springer)
• 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, 2003. doi link - .pdf, 228K (© Springer)
• T. Uustalu. Generalizing substitution.
  Theor. Inform. and Appl., v. 37, n. 4, pp. 315-336, 2003. doi link, article at NUMDAM - .pdf, 240K (© EDP Sciences) //
  Extended abstract in Z. Ésik, A. Ingólfsdóttir, eds., Prel. Proc. of 4th Int. Wksh. on Fixed Points in Computer Science, FICS '02 (Copenhagen, July 2002), BRICS Notes Series NS-02-2, pp. 9-11. Dept. of Computer Science, Univ. of Aarhus, 2002.
• G. Barthe, T. Uustalu. CPS translating inductive and coinductive types (extended abstract).
  In Proc. of 2002 ACM SIGPLAN Wksh. on Partial Evaluation and Semantics-Based Program Manipulation, PEPM '02 (Portland, OR, Jan. 2002) (= ACM SIGPLAN Notices, v. 37, n. 3), pp. 131-142. ACM Press, 2002. doi link - free pdf from ACM DL (via ACM Author-Izer) (© ACM)
• T. Uustalu. (Co)monads from inductive and coinductive types.
  In L. M. Pereira, P. Quaresma, eds., Proc. of 2001 APPIA-GULP-PRODE Joint Conf. on Declarative Programming, AGP '01 (Évora, Sept. 2001), pp. 47-61. Univ. de Évora, 2001.
• 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, Bristol / Portland, OR, 2002. - .pdf, 111K
• T. Uustalu, V. Vene, A. Pardo. Recursion schemes from comonads.
  Nordic J. of Computing, v. 8, n. 3, pp. 366-390, 2001. - .pdf, 318K (© Publ. Assoc. Nordic J. of Computing)
• G. Barthe, M. J. Frade, E. Giménez, L. Pinto, T. Uustalu. Type-based termination of recursive definitions.
  Math. Struct. in Comput. Sci., v. 14, n. 1, pp. 97-141, 2004. doi link - .pdf, 348K (© Cambridge Univ. Press)
• T. Uustalu, V. Vene. Coding recursion a la Mendler (extended abstract).
  In J. Jeuring, ed., Proc. of 2nd Wksh. on Generic Programming, WGP 2000 (Ponte de Lima, July 2000), Techn. Report UU-CS-2000-19, pp. 69-85. Dept. of Comput. Sci., Utrecht Univ., 2000. - .pdf, 237K
• T. Uustalu, V. Vene. Mendler-style inductive types, categorically.
  Nordic J. of Computing, v. 6, n. 3, pp. 343-361, 1999. - .pdf, 486K (© Publ. Assoc. Nordic J. of Computing)
• T. Uustalu, V. Vene. Primitive (co)recursion and course-of-value (co)iteration, categorically.
  Informatica, v. 10, n. 1, pp. 5-26, 1999. article at publisher's website - .pdf, 155K (© Inst. of Math. and Inform.)
• V. Vene, T. Uustalu. Functional programming with apomorphisms (corecursion).
  Proc. of Estonian Acad. of Sci.: Phys., Math., v. 47, n. 3, pp. 147-161, 1998. issue in Google Books - .pdf, 282K (© Estonian Academy Publishers)
• 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 link - .pdf, 296K (accepted author manuscript, © Elsevier Science)
• T. Uustalu, V. Vene. A cube of proof systems for the intuitionistic predicate μ,ν-logic.
  In M. Haveraaen, O. Owe, eds., Selected Papers from 8th Nordic Wksh. on Programming Theory, NWPT '96 (Oslo, Dec. 1996), Research Report 248, pp. 237-246. Inst. for informatikk, Univ. i Oslo, 1997. - .pdf, 255K