| Publication | Date of Publication | Type |
|---|
Failure of cut-elimination in cyclic-proof systems of logic of bunched implications with inductive propositions
Archive for Mathematical Logic | 2026-04-13 | Paper |
Restriction on cut rule in cyclic-proof system for symbolic heaps
Theoretical Computer Science | 2024-11-06 | Paper |
| Completeness of cyclic proofs for symbolic heaps with inductive definitions | 2024-04-19 | Paper |
| Cut elimination for propositional cyclic proof systems with fixed-point operators | 2023-12-20 | Paper |
| Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions | 2023-06-23 | Paper |
Z property for the shuffling calculus
Mathematical Structures in Computer Science | 2023-02-28 | Paper |
Confluence proofs of lambda-mu-calculi by Z theorem
Studia Logica | 2021-12-27 | Paper |
| Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps | 2021-07-06 | Paper |
Confluence for classical logic through the distinction between values and computations
(available as arXiv preprint) | 2021-06-24 | Paper |
| Confluence for classical logic through the distinction between values and computations | 2021-06-24 | Paper |
scientific article; zbMATH DE number 7340562 (Why is no real title available?)
(available as arXiv preprint) | 2021-04-27 | Paper |
| scientific article; zbMATH DE number 7340562 (Why is no real title available?) | 2021-04-27 | Paper |
Compositional Z: confluence proofs for permutative conversion
Studia Logica | 2017-03-02 | Paper |
Strong reduction of combinatory calculus with streams
Studia Logica | 2015-07-02 | Paper |
Reduction system for extensional lambda-mu calculus
Lecture Notes in Computer Science | 2014-07-24 | Paper |
Type checking and inference for polymorphic and existential types in multiple-quantifier and type-free systems
Chicago Journal of Theoretical Computer Science | 2014-05-06 | Paper |
Monadic translation of classical sequent calculus
Mathematical Structures in Computer Science | 2014-04-16 | Paper |
Type checking and typability in domain-free lambda calculi
Theoretical Computer Science | 2012-01-04 | Paper |
Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types
Functional and Constraint Logic Programming | 2010-04-27 | Paper |
Strong normalization proofs by CPS-translations
Information Processing Letters | 2010-01-29 | Paper |
An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
Lecture Notes in Computer Science | 2009-03-10 | Paper |
Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
Computer Science Logic | 2008-11-20 | Paper |
Strong normalization of classical natural deduction with disjunctions
Annals of Pure and Applied Logic | 2008-04-24 | Paper |
Strong normalization proof with CPS-translation for second order classical natural deduction
Journal of Symbolic Logic | 2005-02-09 | Paper |
Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus
Theoretical Computer Science | 2003-01-21 | Paper |
