Bibliography

  1. M. Tatsuta, Monotone Recursive Definition of Predicates and Its Realizability Interpretation, Proceedings of International Conference on Theoretical Aspects of Computer Software, LNCS 526 (1991) 38--52. (Abstract,dvi file)
  2. M. Tatsuta, Program synthesis using realizability, Theoretical Computer Science 90 (1991) 309--353. (Abstract,dvi file)
  3. M. Tatsuta, Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams, Proceedings of International Conference on Fifth Generation Computer Systems (1992) 666--673. (Abstract)
  4. M. Tatsuta, Realizability of Inductive Definitions for Constructive Programming, PhD Thesis, University of Tokyo, 1993. (dvi file)
  5. M. Tatsuta, Uniqueness of normal proofs of minimal formulas, Journal of Symbolic Logic 58 (3) (1993) 789--799. (Abstract,dvi file)
  6. M. Tatsuta, Realizability interpretation of coinductive definitions and program synthesis with streams, Theoretical Computer Science 122 (1994) 119--136. (Abstract,dvi file)
  7. S. Kobayashi and M. Tatsuta, Realizability interpretation of generalized inductive definitions, Theoretical Computer Science 131 (1) (1994) 121--138. (Abstract,dvi file)
  8. M. Tatsuta, Two realizability interpretations of monotone inductive definitions, International Journal of Foundations of Computer Science 5 (1) (1994) 1--21. (Abstract,ps file)
  9. M. Tada and M. Tatsuta, The Function [a/m] in Sharply Bounded Arithmetic, Archive for Mathematical Logic 37 (1997) 51--57. (Abstract)
  10. M. Tatsuta, Uniform Continuity of Graph Model and Partial Function Model, Proceedings of 1997-98 Anuual Meeting of Association for Symbolic Logic (1998) 20--21. (Abstract)
  11. M. Tatsuta, Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis, Proceedings of Fourth International Conference on Mathematics of Program Construction, LNCS 1422 (1998) 338--364. (Abstract,ps file)
  12. M. Tatsuta, Realizability for Constructive Theory of Functions and Classes and Its Application to Program Synthesis, Proceedings of Thirteenth Annual IEEE Symposium on Logic in Computer Science (1998) 358--367. (Abstract,ps file)
  13. M. Tatsuta, Uniqueness of D-normal Proofs, Proceedings of 7th Asian Logic Conference (1999) 41--42. (Abstract)
  14. S. Hirokawa and M. Tatsuta, Long D-normal form yields uniqueness of proofs, Proceedings of Logic Colloqium 2000. (Abstract)
  15. Makoto Tatsuta and Grigori Mints, Second Order Strong Normalization with Permutative Conversions, Annals of Pure and Applied Logic 136 (1-2) (2005) 134--155. (Abstract,pdf file)
  16. Makoto Tatsuta, Second order permutative conversions with Prawitz's strong validity, Progress in Informatics 2 (2005) 41--56. (Abstract,pdf file)
  17. Mariangiola Dezani-Ciancaglini and Makoto Tatsuta, A Behavioural Model for Klop's Calculus, In: Proceedings of Logic, Model and Computer Science 2006, Electronic Notes in Theoretical Computer Science 169 (2007) 19--32. (Abstract)
  18. Makoto Tatsuta and Mariangiola Dezani-Ciancaglini, Normalisation is Insensible to lambda-term Identity or Difference, lambda-term Identity or Difference, In: Proceedings of Twenty First Annual IEEE Symposium on Logic in Computer Science (2006) 327--336. (Abstract)
  19. Makoto Tatsuta, Simple saturated sets for disjunction and second-order existential quantification, In: Proceedings of 8th International Conference on Typed Lambda Calculi and Applications (TLCA 2007), Lecture Notes in Computer Science 4583 (2007) 366--380. (Abstract)
  20. Makoto Tatsuta, The maximum length of mu-reduction in lambda mu-calculus, In: Proceedings of 18th International Conference on Rewriting Techniques and Applications (RTA'07), Lecture Notes in Computer Science 4533 (2007) 359--373. (Abstract)
  21. Stefano Berardi and Makoto Tatsuta, Positive Arithmetic without Exchange is a Subclassical Logic, In: Proceedings of the Fifth Asian Symposium on Programming Languages and Systems (APLAS 2007), Lecture Notes in Computer Science 4807 (2007) 271--285. (Abstract)
  22. Koji Nakazawa and Makoto Tatsuta, Strong normalization of classical natural deduction with disjunctions, Annals of Pure and Applied Logic 153 (1-3) (2008) 21--37. (Abstract)
  23. Makoto Tatsuta, Types for Hereditary Head Normalizing Terms, In: Proceedings of Ninth International Symposium on Functional and Logic Programming (FLOPS 2008), Lecture Notes in Computer Science 4989 (2008) 195--209. (Abstract)
  24. Makoto Tatsuta, Types for Hereditary Permutators, In: Proceedings of Twenty-Third Annual IEEE Symposium on Logic in Computer Science (2008) 83--92. (Abstract)
  25. Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano, Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence, In: Proceedings of 17th EACSL Annual Conference on Computer Science Logic (CSL2008), Lecture Notes in Computer Science 5213 (2008) 478--492. (Abstract)
  26. Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, and Makoto Tatsuta, On Isomorphisms of Intersection Types, In: Proceedings of 17th EACSL Annual Conference on Computer Science Logic (CSL2008), Lecture Notes in Computer Science 5213 (2008) 461--477. (Abstract)
  27. Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, and Hiroshi Nakano, Inhabitation of Existential Types is Decidable in Negation-Product Fragment, In: Proceedings of 2nd International Workshop on Classical Logic and Computation (CLC2008), 2008. (Abstract)
  28. Makoto Tatsuta, Second-Order Logic without Implication nor Disjunction, In: Proceedings of 10th Asian Logic Conference (ALC 10), Bulletin of Symbolic Logic 15 (2) (2009) 262--262. (Abstract)
  29. Koji Nakazawa and Makoto Tatsuta, Type Checking and Inference for Polymorphic and Existential Types, In: Proceedings of The 15th Computing: The Australasian Theory Symposium (CATS2009), Conferences in Research and Practice in Information Technology 94 (2009) 61--69. (Abstract)
  30. Daisuke Kimura and Makoto Tatsuta, Dual Calculus with Inductive and Coinductive Types, In: Proceedings of 20th International Conference on Rewriting Techniques and Applications (RTA 09), Lecture Notes in Computer Science 5595 (2009) 224--238. (Abstract)
  31. Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, and Makoto Tatsuta, On Isomorphisms of Intersection Types, ACM Transactions on Computational Logic 11 (4) (2010) Article No 25. (Abstract)
  32. Makoto Tatsuta, Non-Commutative First-Order Sequent Calculus, In: Proceedings of 18th EACSL Annual Conference on Computer Science Logic (CSL2009), Lecture Notes in Computer Science 5771 (2009) 470--484. (Abstract Preprint)
  33. M. Tatsuta, W.N. Chin, and M.F. Al Ameen, Completeness of Pointer Program Verification by Separation Logic, In: Proceeding of 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009) 179--188. (Abstract)
  34. Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, and Hiroshi Nakano, Inhabitation of Polymorphic and Existential Types, Annals of Pure and Applied Logic 161 (11) (2010) 1390--1399. (Abstract)
  35. Koji Nakazawa and Makoto Tatsuta, Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems, Chicago Journal of Theoretical Computer Science (2010) Article 7. (Abstract)
  36. Stefano Berardi and Makoto Tatsuta, Internal Normalization, Compilation and Decompilation for System F, In: Proceedings of Tenth International Symposium on Functional and Logic Programming (FLOPS 2010), Lecture Notes in Computer Science 6009 (2010) 207--223. (Abstract)
  37. Wontae Choi, Baris Aktemur, Kwangkeun Yi, and Makoto Tatsuta, Static Analysis for Multi-Staged Programs via Unstaging Translation, In: Proceedings of 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2011) 81--92. (Abstract)
  38. Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano, Type Checking and Typability in Domain-Free Lambda Calculi, Theoretical Computer Science 412 (2011) 6193--6207. (Abstract)
  39. Makoto Tatsuta and Ferruccio Damiani, Type Inference for Bimorphic Recursion, In: Proceedings of Second International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2011), Electronic Proceedings in Theoretical Computer Science 54 (2011) 102--115. (Abstract)
  40. Makoto Tatsuta and Stefano Berardi, Non-Commutative Infinitary Peano Arithmetic, In: Proceedings of 20th EACSL Annual Conference on Computer Science Logic (CSL2011), Leibniz International Proceedings in Informatics 12 (2011) 538--552. (Abstract)
  41. Stefano Berardi and Makoto Tatsuta, Internal Models of System F for Decompilation, Theoretical Computer Science 435 (2012) 3--20. (Abstract)
  42. Takayuki Koai and Makoto Tatsuta, Verification of Substitution Theorem Using HOL, Information Processing Society of Japan Transactions on Programming 5 (2) (2012) 88--96. (Abstract)
  43. Daisuke Kimura and Makoto Tatsuta, Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types, Logical Methods in Computer Science 9 (1) (2013) Article 14. (Abstract)
  44. Stefano Berardi and Makoto Tatsuta, Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics, In: Proceedings of 11th International Conference on Typed Lambda Calculi and Applications (TLCA 2013), Lecture Notes in Computer Science 7941 (2013) 61--76. (Abstract)
  45. Makoto Tatsuta and Wei-Ngan Chin, Completeness of Separation Logic with Inductive Definitions for Program Verification, In: Proceeding of 12th International Conference on Software Engineering and Formal Methods (SEFM 2014), Lecture Notes in Computer Science 8702 (2014) 20--34. (Abstract)
  46. Makoto Tatsuta and Daisuke Kimura, Separation Logic with Monadic Inductive Definitions and Implicit Existentials, In: Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS 2015), Lecture Notes in Computer Science 9458 (2015) 69--89. (Abstract)
  47. Makoto Tatsuta and Daisuke Kimura, Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic, In: Proceedings of the 18th JSSST Workshop on Programming and Programming Languages (PPL2016), 15 pages, 2016. (Abstract)
  48. Mahmudul Faisal Al Ameen and Makoto Tatsuta, Completeness for Recursive Procedures in Separation Logic, Theoretical Computer Science 631 (2016) 73-–96. (Abstract)
  49. Stefano Berardi and Makoto Tatsuta, Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proof System, In: Proceeding of 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), Lecture Notes in Computer Science 10203 (2017) 301--317 (EATCS Award for best ETAPS paper). (Abstract)
  50. Daisuke Kimura, Makoto Tatsuta, Decision Procedure for Symbolic Heaps with Arrays, In: Proceedings of the 18th JSSST Workshop on Programming and Programming Languages (PPL2017), 14 pages, 2017. (Abstract)
  51. Stefano Berardi and Makoto Tatsuta, Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic, In: Proceedings of Thirty-Second Annual IEEE Symposium on Logic in Computer Science (LICS2017) (2017), to appear. (Abstract)
  52. Quang Loc Le, Makoto Tatsuta, Jun Sun, and Wei-Ngan Chin, A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic, In: Proceedings of 29th International Conference on Computer-Aided Verification (CAV2017), Lecture Notes in Computer Science 10427 (2017) 495--517. (Abstract)
  53. Daisuke Kimura and Makoto Tatsuta, Decision Procedure for Entailment of Symbolic Heaps with Arrays, In: Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS 2017), Lecture Notes in Computer Science, to appear. (Abstract)

Invited Talks

  1. Makoto Tatsuta, Some Non-Recursively-Enumerable Sets and Their Types, invited talk, Workshop on Constructivism: Logic and Mathematics, May 26--30, 2008, Kanazawa. (Abstract)
  2. Makoto Tatsuta, Realizability of inductive and coinductive definitions, In: Proceedings of JAIST Logic Workshop Series 2015: Constructivism and Computability, invited talk (2015) 16--17. (Abstract)

In Japanese

  1. 小林 聡, 龍田 真, 直観主義的帰納的定義に対する実現可能性解釈, ソフトウェア科学会第6回全国大会論文集 (1989) 113--116.
  2. 龍田 真, 型理論 I, コンピュータソフトェア 8(1) (1991) 25--33.
  3. 龍田 真, 型理論 II, コンピュータソフトェア 8 (2) (1991) 40--46.
  4. 龍田 真, 型理論 III, コンピュータソフトェア 8 (3) (1991) 2--8.
  5. 龍田 真, 型理論 IV, コンピュータソフトェア 8 (4) (1991) 56--68.
  6. 龍田 真, 型理論, (近代科学社, 1992.11) 1--82.
  7. 龍田 真, 構成的集合の実現可能性解釈, 日本ソフトウェア科学会第15回大会論文集 (1998) 189--192.
  8. 龍田 真, 構成的論理とプログラム理論, 1998年度日本数学会秋季総合分科会総合講演企画特別講演アブストラクト (1998) 13--24.
  9. 龍田 真, 構成的集合論の実現可能性とそのプログラム合成への応用, 第1回プログラミングおよびプログラミング言語ワークショップ (1999) 139--143.
  10. 中澤巧爾, 龍田真 選言を含む自然演繹古典論理の強正規化性, 第8回プログラミングおよびプログラミング言語ワークショップ (日本ソフトウェア科学会) (2006) 187--202.
  11. 龍田 真, マリアンジェラ・デザニ, 代入定理と永続強正規化可能性, 日本ソフトウェア科学会第23回全国大会論文集 (2006) 1--6.
  12. 龍田 真, 遺伝的置換子の型とTLCA未解決問題20番, 日本ソフトウェア科学会第25回大会 (2008).
  13. 龍田 真, Wei-Ngan Chin, Mahmudul Faisal Al Ameen, 分離論理によるポインタープログラム検証の完全性, 日本ソフトウェア科学会第27回大会 (2010).

Abstracts


M. Tatsuta, Monotone Recursive Definition of Predicates and Its Realizability Interpretation, Proceedings of International Conference on Theoretical Aspects of Computer Software, LNCS 526 (1991) 38--52.

The main aim of the paper is to construct a logic by which we can formalize properties of programs. Inductive definition or recursive definition plays a very important role for this purpose. Inductive definition has been studied for untyped theories, predicative typed theories and impredicative typed theories. Monotone recursive definition in an untyped theory is studied in this paper. The main point is realizability interpretation of monotone recursive definition. Untyped predicative theory TID0 and TID1 are presented, which have monotone recursive definition of predicates. TID1 has full monotone recursive definition and TID0 has only restricted monotone recursive definition. q-realizability interpretation of TID0 and TID1 is defined. It is proved that the realizability interpretation of TID0 is sound and that the realizability interpretation of TID1 is not sound, though TID1 and its interpretation seem very natural.


M. Tatsuta, Program synthesis using realizability, Theoretical Computer Science 90 (1991) 309--353.

Various theories have been discussed to formalize computation and to develop new methods of programming. The theory EON+mu which has the facility of defining predicates recursively is presented. The theory EON+mu is constructed by adding the facility of recursive definition of predicates to Beeson's EON. Recursively defined data such as lists and trees can be introduced naturally using recursively defined predicates. This facility also enables us to represent a specification formula of a program more easily. In Hayashi's PX, the facility of recursive definition of predicates, called conditional inductive generation, can be used under the syntactical condition that recursive calls of the original predicate occur only in Harrop subformulae. In this paper, a less restricted class of recursively defined predicates can be used. Not only a predicate whose recursive calls occur in Harrop subformulae but a predicate whose recursive calls occur at strictly positive positions is available. This class includes the class of inductive definition with Horn clauses used in Prolog, because of our weaker restriction of strictly positive occurrences of recursive calls. The extended q-realizability interpretation of EON+mu in EON+mu is given to treat recursive definition of predicates. A recursively defined predicate is interpreted as another recursively defined predicate naturally corresponding to the original predicate by this q-realizability interpretation. The soundness of the interpretation is proved in favor of the syntactical condition of recursively defined predicates. An method of program synthesis using q-realizability interpretation in this theory is presented. This method of program synthesis are explained by several examples.


M. Tatsuta, Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams, Proceedings of International Conference on Fifth Generation Computer Systems (1992) 666--673.

The main aim of this paper is to construct a logic by which properties of programs can be formalized for verification, synthesis and transformation of programs. This paper has 2 main points. One point is realizability interpretation of coinductive definitions of predicates. The other point is an extraction of programs which treat streams. An untyped predicative theory TIDnu is presented, which has the facility of coinductive definitions of predicates and is based on a constructive logic. Properties defined by the greatest fixed point, such as streams and the extensional equality of streams, can be formalized by the facility of coinductive definitions of predicates in TIDnu. q-realizability interpretation for TIDnu is defined and the realizability interpretation is proved to be sound. By the realizability interpretation, a program which treats streams can be extracted from a proof of its specification in TIDnu. General program extraction theorem and stream program extraction theorem are presented.


M. Tatsuta, Uniqueness of normal proofs of minimal formulas, Journal of Symbolic Logic 58 (3) (1993) 789--799.

A minimal formula is a formula which is minimal in provable formulas with respect to the substitution relation. This paper shows the followings: (1) A beta-normal proof of a minimal formula of depth 2 is unique in NJ. (2) There exists a minimal formula of depth 3 whose beta-eta-normal proof is not unique in NJ. (3) There exists a minimal formula of depth 3 whose beta-eta-normal proof is not unique in NK.


M. Tatsuta, Realizability interpretation of coinductive definitions and program synthesis with streams, Theoretical Computer Science 122 (1994) 119--136.

The main aim of the paper is to construct a logical system in which properties of programs can be formalized for verification, synthesis and transformation of programs. The paper has 2 main points. One point is a realizability interpretation of coinductive definitions of predicates. The other point is extraction of programs which treat streams. An untyped predicative theory TIDnu is presented, which has the facility of coinductive definitions of predicates and is based on constructive logic. Properties defined by the greatest fixed point, such as streams and the extensional equality of streams, can be formalized by the facility of coinductive definitions of predicates in TIDnu. A q-realizability interpretation for TIDnu is defined and the soundness of the interpretation is proved. By the realizability interpretation, a program which treats streams can be extracted from a proof of its specification in TIDnu. General program extraction theorem and stream program extraction theorem are presented.


S. Kobayashi and M. Tatsuta, Realizability interpretation of generalized inductive definitions, Theoretical Computer Science 131 (1) (1994) 121--138.

Generalized inductive definitions give a way of defining a predicate as the least solution P of the equation P <--> A[P] where a predicate variable P may occur in a formula A[P] positively. This paper gives a q-realizability interpretation of generalized inductive definitions and prove the soundness of the interpretation.


M. Tatsuta, Two realizability interpretations of monotone inductive definitions, International Journal of Foundations of Computer Science 5 (1) (1994) 1--21.

Realizability of monotone inductive definitions is studied to construct a logical system in which recursive data structures and recursive control structures of programs are naturally formalized by using inductive definitions and programs can be produced from constructive proofs by using realizability. Two q-realizability interpretations of monotone inductive definitions are presented. One interpretation is defined so that a realizer of an inductively defined predicate is the same as a realizer of its expansion. It is proved that the interpretation of restricted monotone inductive definitions is sound and that the interpretation of full monotone inductive definitions is not sound, though the interpretation seems very natural. Another interpretation is presented by using the higher order coding and q-realizability for the second order logic. The soundness of this interpretation of full monotone inductive definitions is also proved. To prove this result, greatest-lower-bound inductive definitions are introduced.


M. Tada and M. Tatsuta, The Function [a/m] in Sharply Bounded Arithmetic, Archive for Mathematical Logic 37 (1997) 51--57.

This paper proves that the division operation a/m is provably total in the system S_2^0 of Bounded Arithmetic if and only if m is of the form 2^n for some n.


M. Tatsuta, Uniform Continuity of Graph Model and Partial Function Model, Proceedings of 1997-98 Anuual Meeting of Association for Symbolic Logic (1998) 20--21.

The uniform continuity property MCONT for a partial combinatory algebra with pairing and natural numbers is that there exists a functional which uniformly produces from a type 2 functional its associate in the finite type structure on the algebras. This paper shows that actually either the the partial function model or the graph model does not have MCONT.


M. Tatsuta, Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis, Proceedings of Fourth International Conference on Mathematics of Program Construction, LNCS 1422 (1998) 338--364.

Two realizability interpretations of monotone coinductive definitions are studied. One interpretation is defined so that a realizer of a coinductively defined predicate is the same as that of its expansion. For this interpretation, the paper proves that full monotone coinductive definitions are not sound and restricted monotone coinductive definitions are sound. The other interpreration is based on second order logic and can interpret least-upper-bound coinductive definitions, which is generalization of monotone coinductive definitions. By using these interprerations, the paper shows that a program which treats coinductively defined infinite data structures such as streams can be synthesized from a constructive proof of its specification.


M. Tatsuta, Realizability for Constructive Theory of Functions and Classes and Its Application to Program Synthesis, Proceedings of Thirteenth Annual IEEE Symposium on Logic in Computer Science (1998) 358--367.

This paper gives a q-realizability interpretation for Feferman's constructive theory T0 of functions and classes by using a set completion program and without doubling variables, and proves its soundness. This result solves an open problem proposed by Feferman in 1979. Moreover by using this interpretation we can prove a program extraction theorem for T0, which enables us to use constructive sets of T0 for program synthesis.


M. Tatsuta, Uniqueness of D-normal Proofs, Proceedings of 7th Asian Logic Conference (1999) 41--42.

Number of normal proofs has been studied widely. This paper discusses the notion of D-normal proofs to present one of the weakest condition for uniqueness of normal proofs. This paper shows that a beta-eta-D-normal proof of a formula is unique, and by using this this paper provides another proof of the fact that (1) a beta-eta-normal proof of a formula satisfying the PNN-condition is unique, and (2) in BCK logic, a beta-eta-normal proof of a minimal formula is unique.


S. Hirokawa and M. Tatsuta, Long D-normal form yields uniqueness of proofs, Proceedings of Logic Colloqium 2000.

There have been much interest in the conditions for uniqueness of normal form proofs in intuitionistic logic. [Tatsuta99] introduced a notion of D-normal form proof and showed that D-normal form proof is unique for any implicational formula. But this result means the uniqueness of D-normal form proof. There may be some other normal form proof which is not D-normal. We show that D-normality yields the uniqueness of proofs as long as the long-normal form proofs are concerned.


Makoto Tatsuta and Grigori Mints, Second Order Strong Normalization with Permutative Conversions, Annals of Pure and Applied Logic 136 (1-2) (2005) 134--155.

A simple and complete proof of strong normalization for first and second order intuitionistic natural deduction including disjunction, first-order existence and permutative conversions is given. The paper follows Tait-Girard approach via computability predicates (reducibility) and saturated sets. Strong normalization is first established for a set of conversions of a new kind, then deduced for the standard conversions. Difficulties arising for disjunction are resolved using a new logic where disjunction is restricted to atomic formulas.


Makoto Tatsuta, Second order permutative conversions with Prawitz's strong validity, Progress in Informatics 2 (2005) 41--56.

A clear and complete proof of strong normalization of second order natural deduction with permutative conversions is given by using Prawitz's strong validity. This paper completes Prawitz's original proof.


Mariangiola Dezani-Ciancaglini and Makoto Tatsuta, A Behavioural Model for Klop's Calculus, In: Proceedings of Logic, Model and Computer Science 2006, Electronic Notes in Theoretical Computer Science 169 (2007) 19--32.

A model characterising strong normalisation for Klop's extension of lambda-calculus is presented. The main technical tools for this result are an inductive definition of strongly normalising terms of Klop's calculus and an intersection type system for terms of Klop's calculus.


Makoto Tatsuta and Mariangiola Dezani-Ciancaglini, Normalisation is Insensible to lambda-term Identity or Difference, In: Proceedings of Twenty First Annual IEEE Symposium on Logic in Computer Science (2006) 327--336.

This paper analyses the computational behaviour of lambda-term applications. The properties we are interested in are weak normalisation (i.e. there is a terminating reduction) and strong normalisation (i.e. all reductions are terminating). One can prove that the application of a lambda-term M to a fixed number n of copies of the same arbitrary strongly normalising lambda-term is strongly normalising if and only if the application of M to n different arbitrary strongly normalising lambda-terms is strongly normalising. I.e. one has that M X ... X (n times) is strongly normalising, for an arbitrary strongly normalising X, if and only if M X1 ... Xn is strongly normalising for arbitrary strongly normalising X1,...,Xn. The analogous property holds when replacing strongly normalising by weakly normalising. As an application of the result on strong normalisation the lambda-terms whose interpretation is the top element (in the environment which associates the top element to all variables) of the Honsell-Lenisa model turn out to be exactly the lambda-terms which, applied to an arbitrary number of strongly normalising lambda-terms, produces always strongly normalising lambda-terms. This proof uses a finitary logical description of the model by means of intersection types. This answers an open question stated by Dezani, Honsell and Motohama.


Makoto Tatsuta, Simple saturated sets for disjunction and second-order existential quantification, In: Proceedings of 8th International Conference on Typed Lambda Calculi and Applications (TLCA 2007), Lecture Notes in Computer Science 4583 (2007) 366--380.

This paper gives simple saturated sets for disjunction and second-order existential quantification by using the idea of segments in Prawitz's strong validity. Saturated sets for disjunction are defined by Pi-0-1 comprehension and those for second-order existential quantification are defined by Sigma-1-1 comprehension. Saturated-set semantics and a simple strong normalization proof are given to the system with disjunction, second-order existential quantification, and their permutative conversions. This paper also introduces the contraction property to saturated sets, which gives us saturated sets closed under union. This enables us to have saturated-set semantics for the system with union types, second-order existential types, and their permutative conversions, and prove its strong normalization.


Makoto Tatsuta, The maximum length of mu-reduction in lambda mu-calculus, In: Proceedings of 18th International Conference on Rewriting Techniques and Applications (RTA'07), Lecture Notes in Computer Science 4533 (2007) 359--373.

This paper gives the exact number of maximum length of mu-reduction and permutative conversions of disjunction for an untyped term in lambda mu-calculus with disjunction. This number is described by using induction on the number of symbols in a term.


Stefano Berardi and Makoto Tatsuta, Positive Arithmetic without Exchange is a Subclassical Logic, In: Proceedings of the Fifth Asian Symposium on Programming Languages and Systems (APLAS 2007), Lecture Notes in Computer Science 4807 (2007) 271--285.

This paper shows the equivalence for provability between two infinitary systems with the omega-rule. One system is the positive one-sided fragment of Peano arithmetic without Exchange rules. The other system is two-sided Heyting Arithmetic plus the law of Excluded Middle for Sigma^0_1-formulas, and it includes Exchange. Thus, the logic underlying positive Arithmetic without Exchange, a substructural logic, is shown to be a logic intermediate between Intuitionism and Classical Logic, hence a subclassical logic. As a corollary, the authors derive the equivalence for positive formulas among provability in those two systems and validity in two apparently unrelated semantics: Limit Computable Mathematics, and Game Semantics with 1-backtracking.


Koji Nakazawa and Makoto Tatsuta, Strong normalization of classical natural deduction with disjunctions, Annals of Pure and Applied Logic 153 (1-3) (2008) 21--37.

This paper proves strong normalization of classical natural deduction with disjunction and permutative conversions, by using CPS-translation and augmentations. By them, this paper also proves strong normalization of classical natural deduction with general elimination rules for implication and conjunction, and their permutative conversions. This paper also proves natural deduction can be embedded into natural deduction with general elimination rules, strictly preserving proof normalization.


Makoto Tatsuta, Types for Hereditary Head Normalizing Terms, In: Proceedings of Ninth International Symposium on Functional and Logic Programming (FLOPS 2008), Lecture Notes in Computer Science 4989 (2008) 195--209.

Klop's Problem is finding a type for characterizing hereditary head normalizing terms, that is, lambda-terms whose B\"ohm trees do not contain the bottom. This paper proves that this problem does not have any solution by showing that the set of those terms is not recursively enumerable. This paper also gives a best-possible solution by providing an intersection type system with a countably infinite set of types such that typing in all these types characterizes hereditary head normalizing terms. By using the same technique, this paper also shows that the set of lambda-terms normalizing by infinite reduction is not recursively enumerable.


Makoto Tatsuta, Types for Hereditary Permutators, In: Proceedings of Twenty-Third Annual IEEE Symposium on Logic in Computer Science (2008) 83--92.

This paper answers the open problem of finding a type system that characterizes hereditary permutators. First this paper shows that there does not exist such a type system by showing that the set of hereditary permutators is not recursively enumerable. The set of positive primitive recursive functions is used to prove it. Secondly this paper gives a best-possible solution by providing a countably infinite set of types such that a term has every type in the set if and only if the term is a hereditary permutator. By the same technique for the first claim, this paper also shows that a set of normalizing terms in infinite lambda-calculus is not recursively enumerable if it contains some term having a computable infinite path, and shows the set of streams is not recursively enumerable.


Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano, Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence, In: Proceedings of 17th EACSL Annual Conference on Computer Science Logic (CSL2008), Lecture Notes in Computer Science 5213 (2008) 478--492.

This paper shows undecidability of type-checking and type-inference problems in domain-free typed lambda-calculi with existential types: a negation-conjunction fragment, and an implicational fragment. These are proved by reducing type-checking and type-inference problems of the domain-free polymorphic typed lambda-calculus to those of the lambda-calculi with existential types by continuation passing style translations.


Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, and Makoto Tatsuta, On Isomorphisms of Intersection Types, In: Proceedings of 17th EACSL Annual Conference on Computer Science Logic (CSL2008), Lecture Notes in Computer Science 5213 (2008) 461--477.

The study of type isomorphisms for different lambda calculi started over twenty years ago, and a very wide body of knowledge has been established, both in terms of results and in terms of techniques. A notable missing piece of the puzzle was the characterization of type isomorphisms in the presence of intersection types. While at first thought this may seem to be a simple exercise, it turns out that not only finding the right characterization is not simple, but that the very notion of isomorphism in intersection types is an unexpectedly original element in the previously known landscape, breaking most of the known properties of isomorphisms of the typed lambda calculus. In particular, types that are equal in the standard models of intersection types may be non-isomorphic.


Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, and Hiroshi Nakano, Inhabitation of Existential Types is Decidable in Negation-Product Fragment, In: Proceedings of 2nd International Workshop on Classical Logic and Computation (CLC2008), 2008.

This paper shows the inhabitation in the lambda calculus with negation, product, and existential types is decidable. This is proved by showing existential quantification can be eliminated and reducing the problem to provability in intuitionistic propositional logic. By the same technique, this paper also shows existential quantification followed by negation can be replaced by a specific witness in both that system and the system with implication and bottom.


Makoto Tatsuta, Second-Order Logic without Implication nor Disjunction, In: Proceedings of 10th Asian Logic Conference (ALC 10), Bulletin of Symbolic Logic 15 (2) (2009) 262--262.

This paper investigates the system obtained from the second-order natural deduction by removing implication and disjunction, and shows (1) the decidability of its provability, (2) Glivenko's theorem, and (3) Double Negation Shift. This paper also gives a simpler proof to (4) implication from negation of universal quantification to existential quantification of negation, and (5) equivalence of provability of a formula without assumptions in this system and the classical logic obtained from this system.


Makoto Tatsuta, Some Non-Recursively-Enumerable Sets and Their Types, invited talk, Workshop on Constructivism: Logic and Mathematics, May 26--30, 2008, Kanazawa.

Klop's Problem and TLCA open problem 20 were soloved recently by using the same techniques, coding primitive recursive functions by infinite objects and a countably infinite set of types. This talk discusses these techniques and gives future directions. Klop's Problem was finding a type for characterizing hereditary head normalizing terms, that is, lambda-terms whose Bohm trees do not contain the bottom. In the FLOPS2008 conference paper, Tatsuta proved that this problem does not have any solution by showing that the set of those terms is not recursively enumerable. The paper also gave a best-possible solution by providing an intersection type system with a countably infinite set of types such that typing in all these types characterizes hereditary head normalizing terms. TLCA open problem 20 was a problem of finding a type system that characterizes hereditary permutators. In the LICS2008 conference paper, Tatsuta showed that there does not exist such a type system by showing that the set of hereditary permutators is not recursively enumerable. Secondly this paper gave a best-possible solution by providing a countably infinite set of types such that a term has every type in the set if and only if the term is a hereditary permutator. This talk explains these techniques can be used to investigate types for streams, coinductively defined data, and infinite lambda-calculus.


Koji Nakazawa and Makoto Tatsuta, Type Checking and Inference for Polymorphic and Existential Types, In: Proceedings of The 15th Computing: The Australasian Theory Symposium (CATS2009), Conferences in Research and Practice in Information Technology 94 (2009) 61--69.

This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be undecidable, and then it is proved that type inference is undecidable in the negation, conjunction, and existence fragment of the domain-free typed lambda calculus. Secondly, their variants with multiple quantifier rules are introduced, and their type checking and type inference are proved to be undecidable. Finally, it is proved that we can reduce undecidability of type checking and type inference problems in the Curry-style lambda calculus in negation, conjunction, and existential fragment to undecidability of those problems in another variant of the domain-free polymorphic lambda calculus.


Daisuke Kimura and Makoto Tatsuta, Dual Calculus with Inductive and Coinductive Types, In: Proceedings of 20th International Conference on Rewriting Techniques and Applications (RTA 09), Lecture Notes in Computer Science 5595 (2009) 224--238.

This paper gives an extension of Dual Calculus by introducing inductive types and coinductive types. The same duality as Dual Calculus is shown to hold in the new system, that is, this paper presents its involution for the new system and proves that it preserves both typing and reduction. The duality between inductive types and coinductive types is shown by the existence of the involution that maps an inductive type and a coinductive type to each other. The strong normalization in this system is also proved. First, strong normalization in second-order Dual Calculus is shown by translating it into second-order symmetric lambda calculus. Next, strong normalization in Dual Calculus with inductive and coinductive types is proved by translating it into second-order Dual Calculus.


Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, and Makoto Tatsuta, On Isomorphisms of Intersection Types, ACM Transactions on Computational Logic 11 (4) (2010) Article No 25.

The study of type isomorphisms for different lambda-calculi started over twenty years ago, and a very wide body of knowledge has been established, both in terms of results and in terms of techniques. A notable missing piece of the puzzle was the characterization of type isomorphisms in the presence of intersection types. While at first thought this may seem to be a simple exercise, it turns out that not only finding the right characterization is not simple, but that the very notion of isomorphism in intersection types is an unexpectedly original element in the previously known landscape, breaking most of the known properties of isomorphisms of the typed lambda-calculus. In particular, isomorphism is not a congruence and types that are equal in the standard models of intersection types may be non-isomorphic.


Makoto Tatsuta, Non-Commutative First-Order Sequent Calculus, In: Proceedings of 18th EACSL Annual Conference on Computer Science Logic (CSL2009), Lecture Notes in Computer Science 5771 (2009) 470--484.

This paper investigates a non-commutative first-order sequent calculus NCLK. For that, this paper extends a non-commutative positive fragment to a full first-order sequent calculus LK- having antecedent-grouping and no right exchange rule. This paper shows (1) NCLK is equivalent to LJ, (2) NCLK with the exchange rule is equivalent to LK, (3) LK- is equivalent to LJ, and (4) translations between LK- and NCLK.


M. Tatsuta, W.N. Chin, and M.F. Al Ameen, Completeness of Pointer Program Verification by Separation Logic, In: Proceeding of 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009) 179--188.

Reynolds' separation logical system for pointer program verification is investigated. This paper proves its completeness theorem as well as the expressiveness theorem that states the weakest precondition of every program and every assertion can be expressed by some assertion. This paper also introduces the predicate that represents the next new cell, and proves the completeness and the soundness of the extended system under deterministic semantics.


Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, and Hiroshi Nakano, Inhabitation of Polymorphic and Existential Types, Annals of Pure and Applied Logic 161 (11) (2010) 1390--1399.

This paper shows the inhabitation problem in the lambda calculus with negation, product, polymorphic, and existential types is decidable, where the inhabitation problem asks whether there exists some term that belongs to a given type. In order for that, this paper proves the decidability of the provability in the logical system defined from the second-order natural deduction by removing implication and disjunction. This is proved by showing the quantifier elimination theorem and reducing the problem to the provability in propositional logic. The magic formulas are used for quantifier elimination so that they replace quantifiers. As a byproduct, this paper also shows the second-order witness theorem which states a quantifier followed by negation can be replaced by a witness obtained only from the formula. As a corollary of the main results, this paper also shows Glivenko's theorem, Double Negation Shift, and conservativeness for anticedent-empty sequents between the logical system and its classical version.


Koji Nakazawa and Makoto Tatsuta, Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems, Chicago Journal of Theoretical Computer Science (2010) Article 7.

A multiple quantifier is a quantifier having inference rules that introduce or eliminate arbitrary number of quantifiers by one inference. This paper introduces the lambda calculus with negation, conjunction, and multiple existential quantifiers, and the lambda calculus with implication and multiple universal quantifiers. Their type checking and type inference are proved to be undecidable. This paper also shows that the undecidability of type checking and type inference in the type-free-style lambda calculus with negation, conjunction, and existence is reduced to the undecidability of type checking and type inference in the type-free-style polymorphic lambda calculus.


Stefano Berardi and Makoto Tatsuta, Internal Normalization, Compilation and Decompilation for System F, In: Proceedings of Tenth International Symposium on Functional and Logic Programming (FLOPS 2010), Lecture Notes in Computer Science 6009 (2010) 207--223. This paper defines a family of terms of System F which is a decompiler-normalizer for an image of System F by some injective interpretation in System F. We clarify the relationship among these terms, normalization by evaluation, and beta-eta-complete models of F.
Wontae Choi, Baris Aktemur, Kwangkeun Yi, and Makoto Tatsuta, Static Analysis for Multi-Staged Programs via Unstaging Translation, In: Proceedings of 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2011) 81--92.

Static analysis of multi-staged programs is challenging because the basic assumption of conventional static analysis no longer holds: the program text itself is no longer a fixed static entity, but rather a dynamically constructed value. This article presents a semantic-preserving translation of multi-staged call-by-value programs into unstaged programs and a static analysis framework based on this translation. The translation is semantic-preserving in that every small-step reduction of a multi-staged program is simulated by the evaluation of its unstaged version. Thanks to this translation we can analyze multi-staged programs with existing static analysis techniques that have been developed for conventional unstaged programs: We first apply the unstaging translation, then we apply conventional static analysis to the unstaged version, and finally we cast the analysis results back in terms of the original staged program. Our translation is practical enough; it handles staging constructs that have been evolved to be useful in practice (typified in Lisp's quasi-quotation): open code as values, unrestricted operations on references and intentional variable-capturing substitutions.


Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano, Type Checking and Typability in Domain-Free Lambda Calculi, Theoretical Computer Science 412 (2011) 6193--6207.

This paper shows (1) the undecidability of the type checking and the typability problems in the domain-free lambda calculus with negation, product, and existential types, (2) the undecidability of the typability problem in the domain-free polymorphic lambda calculus, and (3) the undecidability of the type checking and the typability problems in the domain-free lambda calculus with function and existential types. The first and the third results are proved by the second result and CPS translations that reduce those problems in the domain-free polymorphic lambda calculus to those in the the domain-free lambda calculi with existential types. The key idea is the conservativity of the domain-free lambda calculi with existential types over the images of the translations.


Makoto Tatsuta and Ferruccio Damiani, Type Inference for Bimorphic Recursion, In: Proceedings of Second International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2011), Electronic Proceedings in Theoretical Computer Science 54 (2011) 102--115.

This paper proposes bimorphic recursion, which is restricted polymorphic recursion such that every recursive call in the body of a function definition has the same type. Bimorphic recursion allows us to assign two different types to a recursively defined function: one is for its recursive calls and the other is for its calls outside its definition. Bimorphic recursion in this paper can be nested. This paper shows bimorphic recursion has principal types and decidable type inference. Hence bimorphic recursion gives us flexible typing for recursion with decidable type inference. This paper also shows that its typability becomes undecidable because of nesting of recursions when one removes the instantiation property from the bimorphic recursion.


Makoto Tatsuta and Stefano Berardi, Non-Commutative Infinitary Peano Arithmetic, In: Proceedings of 20th EACSL Annual Conference on Computer Science Logic (CSL2011), Leibniz International Proceedings in Informatics 12 (2011) 538--552.

Does there exist any sequent calculus such that it is a subclassical logic and it becomes classical logic when the exchange rules are added? The first contribution of this paper is answering this question for infinitary Peano arithmetic. This paper defines infinitary Peano arithmetic with non-commutative sequents, called non-commutative infinitary Peano arithmetic, so that the system becomes equivalent to Peano arithmetic with the omega-rule if the the exchange rule is added to this system. This system is unique among other non-commutative systems, since all the logical connectives have standard meaning and specifically the commutativity for conjunction and disjunction is derivable. This paper shows that the provability in non-commutative infinitary Peano arithmetic is equivalent to Heyting arithmetic with the omega rule and the law of excluded middle for Sigma-0-1 formulas. Thus, non-commutative infinitary Peano arithmetic is shown to be a subclassical logic. The cut elimination theorem in this system is also proved. The second contribution of this paper is introducing infinitary Peano arithmetic having antecedent-grouping and no right exchange rules. The first contribution of this paper is achieved through this system. This system is obtained from the positive fragment of infinitary Peano arithmetic without the exchange rules by extending it from a positive fragment to a full system, preserving its 1-backtracking game semantics. This paper shows that this system is equivalent to both non-commutative infinitary Peano arithmetic, and Heyting arithmetic with the omega rule and the Sigma-0-1 excluded middle.


Stefano Berardi and Makoto Tatsuta, Internal Models of System F for Decompilation, Theoretical Computer Science 435 (2012) 3--20.

This paper considers Girard's internal coding of each term of System F by some term of a code type. This coding is the type-erasing coding definable already in the simply typed lambda-calculus using only abstraction on term variables. It is shown that there does not exist any decompiler for System F in System F, where the decompiler maps a term of System F to its code. An internal model of F is given by interpreting each type of F by some type equipped with maps between the type and the code type. This paper gives a decompiler-normalizer for this internal model in F, where the decompiler-normalizer maps any term of the internal model to the code of its normal form. It is also shown that for any model of F the composition of this internal model and the model produces another model of F whose equational theory is below untyped beta-eta-equality.


Takayuki Koai and Makoto Tatsuta, Verification of Substitution Theorem Using HOL, Information Processing Society of Japan Transactions on Programming 5 (2) (2012) 88--96.

Substitution Theorem is a new theorem in untyped lambda calculus, which was proved in 2006. This theorem states that for a given lambda term and given free variables in it, the term becomes weakly normalizing when we substitute arbitrary weakly normalizing terms for these free variables, if the term becomes weakly normalizing when we substitute a single arbitrary weakly normalizing term for these free variables. This paper formalizes and verifies this theorem by using the higher-order theorem prover HOL. A control path, which is the key notion in the proof, explicitly uses names of bound variables in lambda terms, and it is defined only for lambda terms without bound variable renaming. The lambda terms without bound variable renaming are formalized by using the HOL package based on contextual alpha-equivalence. The verification uses 10119 lines of HOL code and 326 lemmas.


Daisuke Kimura and Makoto Tatsuta, Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types, Logical Methods in Computer Science 9 (1) (2013) Article 14.

This paper extends the dual calculus with inductive types and coinductive types. The paper first introduces a non-deterministic dual calculus with inductive and coinductive types. Besides the same duality of the original dual calculus, it has the duality of inductive and coinductive types, that is, the duality of terms and coterms for inductive and coinductive types, and the duality of their reduction rules. Its strong normalization is also proved, which is shown by translating it into a second-order dual calculus. The strong normalization of the second-order dual calculus is proved by translating it into the second-order symmetric lambda calculus. This paper then introduces a call-by-value system and a call-by-name system of the dual calculus with inductive and coinductive types, and shows the duality of call-by-value and call-by-name, their Church-Rosser property, and their strong normalization. Their strong normalization is proved by translating them into the non-deterministic dual calculus with inductive and coinductive types.


Stefano Berardi and Makoto Tatsuta, Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics, In: Proceedings of 11th International Conference on Typed Lambda Calculi and Applications (TLCA 2013), Lecture Notes in Computer Science 7941 (2013) 61--76.

This paper introduces a game semantics for Arithmetic with various sub-classical logics that have implication as a primitive connective. This semantics clarifies the infinitary sequent calculus that the authors proposed for intuitionistic arithmetic with Excluded Middle for Sigma-0-1-formulas, a formal system motivated by proof mining and by the study of monotonic learning, for which no game semantics is known. This paper proposes games with Sequential Backtracking, and proves that they provide a sound and complete semantics for the logical system and other various subclassical logics. In order for that, this paper also defines a one-sided version of the logical system, whose proofs have a tree isomorphism with respect to the winning strategies of the game semantics.


Makoto Tatsuta and Wei-Ngan Chin, Completeness of Separation Logic with Inductive Definitions for Program Verification, In: Proceeding of 12th International Conference on Software Engineering and Formal Methods (SEFM 2014), Lecture Notes in Computer Science 8702 (2014) 20--34.

This paper extends Reynolds' separation logical system for pointer-based while program verification by adding inductive definitions. Inductive definitions give us a great advantage for verification, since they enable us for example, to formalize linked lists and to support the lemma reasoning mechanism. This paper proves its completeness theorem that states that every true asserted program is provable in the logical system. In order to prove its completeness, this paper shows an expressiveness theorem that states the weakest precondition of every program and every assertion can be expressed by some assertion.


Makoto Tatsuta and Daisuke Kimura, Separation Logic with Monadic Inductive Definitions and Implicit Existentials, In: Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS 2015), Lecture Notes in Computer Science 9458 (2015) 69--89.

This paper proves the decidability of entailments in separation logic with monadic inductive definitions and implicit existentials. This system is obtained from the bounded-treewidth separation logic SLRDbtw of Iosif et al in 2013 by adding implicit existential variables and restricting inductive definitions to monadic ones. The system proposed in this paper is a decidable system where one can use general recursive data structures with pointers as data, such as lists of pointers. The key idea is to reduce the problem to the decidability of SLRDbtw, by assigning local addresses or some distinguished address to implicit existential variables so that the resulting definition clauses satisfy the establishment condition of SLRDbtw. This paper also proves the undecidability of the entailments when one adds implicit existentials to SLRDbtw. This shows that the implicit existentials are critical for the decidability.


Makoto Tatsuta and Daisuke Kimura, Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic, In: Proceedings of the 18th JSSST Workshop on Programming and Programming Languages (PPL2016), 15 pages, 2016.

This paper discusses implementation of an entailment checker for the logical system of symbolic heaps with monadic inductive definitions proposed by the same authors. The logical system is worth implementation, since its entailments are decidable and it has general inductive definitions as well as implicit existentials. The implementation is done by translating the system into monadic second-order logic and checking the resulting MSO formula by the decision procedure MONA developed in Denmark. This paper discusses the equivalence theorem of the translation. This paper also explains some ideas for efficient implementation, in particular, optimization of equivalence relation on tree nodes.


Mahmudul Faisal Al Ameen and Makoto Tatsuta, Completeness for Recursive Procedures in Separation Logic, Theoretical Computer Science 631 (2016) 73-–96.

This paper proves the completeness of an extension of Hoare's logic and separation logic for pointer programs with mutual recursive procedures. This paper shows the expressiveness of the assertion language as well. This paper achieves a new system by introducing two new inference rules, and removes an axiom that is unsound in separation logic and other redundant inference rules for showing completeness. It introduces a novel expression that is used to describe complete information of a given state in a precondition. This work also uses the necessary and sufficient precondition of a program for the abort-free execution, which enables us to utilize strongest postconditions.


Stefano Berardi and Makoto Tatsuta, Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proof System, In: Proceeding of 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), Lecture Notes in Computer Science 10203 (2017) 301--317 (EATCS Award for best ETAPS paper).

A cyclic proof system, called CLKIDomega, gives us another way of representing inductive definitions and efficient proof search. The 2011 paper by Brotherston and Simpson showed that the provability of CLKIDomega includes the provability of Martin-Lof's system of inductive definitions, called LKID, and conjectured the equivalence. Since then, the equivalence has been left an open question. This paper shows that CLKIDomega and LKID are indeed not equivalent. This paper considers a statement called 2-Hydra in these two systems with the first-order language by 0, the successor, the natural number predicate, and a binary predicate symbol used to express 2-Hydra. This paper shows that the 2-Hydra statement is provable in CLKIDomega, but the statement is not provable in LKID, by constructing some Henkin model where the statement is false.


Daisuke Kimura, Makoto Tatsuta, Decision Procedure for Symbolic Heaps with Arrays, In: Proceedings of the 18th JSSST Workshop on Programming and Programming Languages (PPL2017), 14 pages, 2017.

This paper proves the decidability of validity of entailments in the logical system of symbolic heaps with arrays. This paper also discusses an implementation of a decision procedure based on it. Separation logic is successfully used for verification of memory safety of pointer programs. However, dynamically allocated arrays have been investigated only by a manuscript by Brotherston et al, and they discuss only a separation logic system that contains arrays and does not contain the points-to predicate. This paper shows the first decidability result for the logical system that contains both arrays and the points-to predicate. This paper first gives a procedure that checks if a given entailment in the logical system is valid. Our decision procedure reduces the validity of entailments with arrays to that of Presburger arithmetic. Then the correctness of the procedure is shown, by induction on the execution steps of the procedure. The implementation of our decision procedure is also discussed. It first translates the given entailment into the corresponding formula in Presburger arithmetic. Finally the validity of the formula is checked by an external SMT-solver. The straightforward implementation is not so efficient. We also discuss some possible improvements towards a more efficient implementation.


Stefano Berardi and Makoto Tatsuta, Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic, In: Proceedings of Thirty-Second Annual IEEE Symposium on Logic in Computer Science (LICS2017) (2017), to appear.

A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2011 paper by Brotherston and Simpson showed that the provability of CLKID-omega includes the provability of the classical system of Martin-Lof's inductive definitions, called LKID, and conjectured the equivalence. By this year the equivalence has been left an open question. In general, the conjecture was proved to be false in FoSSaCS 2017 paper by Berardi and Tatsuta. However, if we restrict both systems to only the natural number inductive predicate and add Peano arithmetic to both systems, the conjecture is proved to be true in FoSSaCS 2017 paper by Simpson. This paper shows that if we add arithmetic to both systems, they become equivalent, namely, the conjecture holds. The result of this paper includes that of the paper by Simpson as a special case. In order to construct a proof of LKID for a given cyclic proof, this paper shows every bud in the cyclic proof is provable in LKID, by cutting the cyclic proof into subproofs such that in each subproof the conclusion is a companion and the assumptions are buds. The global trace condition gives some induction principle, by using an extension of Podelski-Rybalchenko termination theorem from well-foundedness to induction schema. In order to show this extension, this paper also shows that infinite Ramsey theorem is formalizable in Peano arithmetic.


Quang Loc Le, Makoto Tatsuta, Jun Sun, and Wei-Ngan Chin, A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic, In: Proceedings of 29th International Conference on Computer-Aided Verification (CAV2017), Lecture Notes in Computer Science 10427 (2017) 495--517.

We consider the satisfiability problem for a fragment of separation logic including inductive predicates with shape and arithmetic properties. We show that the fragment is decidable if the arithmetic properties can be represented as semilinear sets. Our decision procedure is based on a novel algorithm to infer a finite representation for each inductive predicate which precisely characterises its satisfiability. Our analysis shows that the proposed algorithm runs in exponential time in the worst case. We have implemented our decision procedure and integrated it into an existing verification system. Our experiment on benchmarks shows that our procedure helps to verify the benchmarks effectively.


Daisuke Kimura and Makoto Tatsuta, Decision Procedure for Entailment of Symbolic Heaps with Arrays, In: Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS 2017), Lecture Notes in Computer Science, to appear.

This paper gives a decision procedure for the validity of entailment of symbolic heaps in separation logic with Presburger arithmetic and arrays. The correctness of the decision procedure is proved under the condition that sizes of arrays in the succedent are not existentially bound. This condition is independent of the condition proposed by the CADE-2017 paper by Brotherston et al, namely, one of them does not imply the other. For improving efficiency of the decision procedure, some techniques are also presented. The main idea of the decision procedure is a novel translation of an entailment of symbolic heaps into a formula in Presburger arithmetic, and to combine it with an external SMT solver. This paper also gives experimental results by an implementation, which shows that the decision procedure works efficiently enough to use.


Makoto Tatsuta, Realizability of inductive and coinductive definitions, In: Proceedings of JAIST Logic Workshop Series 2015: Constructivism and Computability, invited talk (2015) 16--17.

This talk defines g-realizability and r-realizability of Mendler-style nonmonotonic inductive and coinductive definitions, and proves their soundness.