| Function Pointer Eliminator for C Programs | 0 | 0.34 | 2021 |
| Completeness and expressiveness of pointer program verification by separation logic | 0 | 0.34 | 2019 |
| Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs. | 0 | 0.34 | 2019 |
| Decidability For Entailments Of Symbolic Heaps With Arrays | 0 | 0.34 | 2018 |
| Completeness of Cyclic Proofs for Symbolic Heaps. | 0 | 0.34 | 2018 |
| Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System. | 2 | 0.39 | 2017 |
| Micro-Clustering By Data Polishing | 0 | 0.34 | 2017 |
| Analysis and Verification of Pointer Programs (NII Shonan Meeting 2017-14). | 0 | 0.34 | 2017 |
| Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic. | 2 | 0.36 | 2016 |
| Completeness for recursive procedures in separation logic. | 0 | 0.34 | 2016 |
| Separation Logic With Monadic Inductive Definitions And Implicit Existentials | 2 | 0.37 | 2015 |
| Micro-Clustering: Finding Small Clusters in Large Diversity | 2 | 0.48 | 2015 |
| Completeness of Separation Logic with Inductive Definitions for Program Verification. | 2 | 0.36 | 2014 |
| Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics. | 0 | 0.34 | 2013 |
| Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types | 3 | 0.42 | 2013 |
| Internal models of system F for decompilation | 0 | 0.34 | 2012 |
| Non-Commutative Infinitary Peano Arithmetic. | 3 | 0.39 | 2011 |
| Type checking and typability in domain-free lambda calculi | 0 | 0.34 | 2011 |
| Type Inference For Bimorphic Recursion | 0 | 0.34 | 2011 |
| Inhabitation of polymorphic and existential types | 2 | 0.41 | 2010 |
| Internal normalization, compilation and decompilation for system Fβη | 1 | 0.42 | 2010 |
| On isomorphisms of intersection types | 3 | 0.44 | 2010 |
| Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems. | 0 | 0.34 | 2010 |
| Completeness of Pointer Program Verification by Separation Logic | 3 | 0.39 | 2009 |
| Type checking and inference for polymorphic and existential types | 2 | 0.39 | 2009 |
| Non-commutative first-order sequent calculus | 1 | 0.36 | 2009 |
| Dual Calculus with Inductive and Coinductive Types | 3 | 0.44 | 2009 |
| Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence | 10 | 0.61 | 2008 |
| Types for Hereditary Permutators | 1 | 0.36 | 2008 |
| Types for hereditary head normalizing terms | 2 | 0.65 | 2008 |
| Strong normalization of classical natural deduction with disjunctions | 3 | 0.41 | 2008 |
| Simple saturated sets for disjunction and second-order existential quantification | 10 | 0.67 | 2007 |
| A Behavioural Model for Klop's Calculus | 2 | 0.50 | 2007 |
| Positive arithmetic without exchange is a subclassical logic | 4 | 0.65 | 2007 |
| The maximum length of mu-reduction in lambda mu-calculus | 0 | 0.34 | 2007 |
| Normalisation is Insensible to \lambda-Term Identity or Difference | 4 | 0.65 | 2006 |
| A simple proof of second-order strong normalization with permutative conversions | 4 | 0.50 | 2005 |
| Strong normalization proof with CPS-translation for second order classical natural deduction | 7 | 0.69 | 2003 |
| Corrigendum to "Strong normalization proof with CPS-translation for second order classical natural deduction | 0 | 0.34 | 2003 |
| Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis | 5 | 0.46 | 1998 |
| The Function [A/M] In Sharply Bounded Arithmetic | 0 | 0.34 | 1997 |
| Two Realizability Interpretations of Monotone Inductive Definitions | 4 | 0.54 | 1994 |
| Realizability interpretation of generalized inductive definitions | 6 | 0.78 | 1994 |
| Realizability interpretation of coinductive definitions and program synthesis with streams | 6 | 0.91 | 1994 |
| Uniqueness Of Normal Proofs Of Minimal Formulas | 1 | 0.46 | 1993 |
| Program synthesis using realizability | 8 | 1.73 | 1991 |
| Monotone Recursive Definition of Predicates and Its Realizability Interpretation | 3 | 0.77 | 1991 |
