| Publication | Date of Publication | Type |
|---|
Logic of refinement types
Lecture Notes in Computer Science | 2023-12-08 | Paper |
Singleton, union and intersection types for program extraction
Lecture Notes in Computer Science | 2022-08-16 | Paper |
Games with 1-backtracking
Annals of Pure and Applied Logic | 2011-08-26 | Paper |
| Can proofs be animated by games? | 2007-07-20 | Paper |
Mathematics based on incremental learning -- excluded middle and inductive inference
Theoretical Computer Science | 2006-03-20 | Paper |
Typed Lambda Calculi and Applications
Lecture Notes in Computer Science | 2005-11-11 | Paper |
| scientific article; zbMATH DE number 2085171 (Why is no real title available?) | 2004-08-09 | Paper |
| scientific article; zbMATH DE number 1966601 (Why is no real title available?) | 2003-08-18 | Paper |
| scientific article; zbMATH DE number 1966517 (Why is no real title available?) | 2003-08-18 | Paper |
| scientific article; zbMATH DE number 1948150 (Why is no real title available?) | 2003-07-10 | Paper |
| scientific article; zbMATH DE number 1783013 (Why is no real title available?) | 2002-08-18 | Paper |
Towards the animation of proofs -- testing proofs by examples
Theoretical Computer Science | 2002-03-03 | Paper |
Formalized mathematics, proof animation, and limit computable mathematics
RIMS Kokyuroku | 2001-09-23 | Paper |
| scientific article; zbMATH DE number 1231518 (Why is no real title available?) | 1998-12-13 | Paper |
| scientific article; zbMATH DE number 1222086 (Why is no real title available?) | 1998-11-11 | Paper |
| scientific article; zbMATH DE number 1047956 (Why is no real title available?) | 1997-11-05 | Paper |
A NEW FORMALIZATION OF FEFERMAN’S SYSTEM OF FUNCTIONS AND CLASSES AND ITS RELATION TO FREGE STRUCTURE
International Journal of Foundations of Computer Science | 1995-12-03 | Paper |
Singleton, union, and intersection types for program extraction
Information and Computation | 1994-05-05 | Paper |
| scientific article; zbMATH DE number 218497 (Why is no real title available?) | 1993-06-29 | Paper |
Adjunction of semifunctors: Categorical structures in nonextensional lambda calculus
Theoretical Computer Science | 1985-01-01 | Paper |
Self-similar sets as Tarski's fixed points
Publications of the Research Institute for Mathematical Sciences, Kyoto University | 1985-01-01 | Paper |
Extracting Lisp programs from constructive proofs: A formal theory of constructive mathematics based on Lisp
Publications of the Research Institute for Mathematical Sciences, Kyoto University | 1983-01-01 | Paper |
| scientific article; zbMATH DE number 3811561 (Why is no real title available?) | 1982-01-01 | Paper |
| scientific article; zbMATH DE number 3784882 (Why is no real title available?) | 1981-01-01 | Paper |
Derived rules related to a constructive theory of metric spaces in intuitionistic higher order arithmetic without countable choice
Annals of Mathematical Logic | 1980-01-01 | Paper |
| scientific article; zbMATH DE number 3652333 (Why is no real title available?) | 1979-01-01 | Paper |
| scientific article; zbMATH DE number 3637861 (Why is no real title available?) | 1977-01-01 | Paper |
Some derived rules of intuitionistic second order arithmetic
Proceedings of the Japan Academy, Series A, Mathematical Sciences | 1977-01-01 | Paper |
A note on provable well-orderings in first order systems with infinitary inference rules
Tsukuba Journal of Mathematics | 1977-01-01 | Paper |
