This directory contains some papers by Susumu Hayashi.

Contents

1. CatAlgSpec.*

    Categories for algebraic specifications,
    Vol. 1, Advances in Software Science and Technology, pp. 169-185, 1989.

 A survey on category theory and algebraic specifications.

2. Heyting88.*

    Constructive Mathematics and Computer-Aided Reasoning Systems,
    MATHEMATICAL LOGIC, P.P. Petkov ed., Plenum Press, New York, 1990.

 A survey on proof checkers on constructive mathematics.

3. SUIT.*

    Singleton, Union and Intersection Types for Program Extraction,
    to appear in Information and Computation.

 An extended version of the paper on Singleton, Union and Intersection
 Types appeared in the proceeding of TACS '91, Sendai, Japan.

4. TransTypes.*

    Interpretations of transfinite recursion and parametric
    abstraction in types, Mariko Yasugi and Susumu Hayashi,
    to appear in Words, Languages and Combinatrics II, M. Ito and
    H. Jurgensen, eds., World Scientific Publish. Co., Singapore.

 A paper on Yasugi's type theory for subsystems of second order analysis. 
 A joint work with Mariko Yasugi.

5. NijmegenBRA93.*

    Logic of refinement types

 A corrected version of the paper appeared in the informal electric
 proceedings of the BRA workshop "Types for Proofs and Programs,"
 June, Nijmegen, 1993, updated on Dec 16 '93. The proceedings are
 found in ../../pub/NijmegenMeeting. 

 This paper investigates logic of refinement types. An open problem
 is posed. Look at and try it!