Logic of refinement types

DOI10.1007/3-540-58085-9_74zbMath1527.68040DBLPconf/types/Hayashi93OpenAlexW1512120669WikidataQ55966764 ScholiaQ55966764MaRDI QIDQ6083692

Susumu Hayashi

Publication date: 8 December 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58085-9_74

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40) Type theory (03B38)

Related Items (1)

Unnamed Item

Cites Work

• Adjunction of semifunctors: Categorical structures in nonextensional lambda calculus
• The calculus of constructions
• First order categorical logic. Model-theoretical methods in the theory of topoi and related categories
• Synthesis of ML programs in the system Coq
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Semantics of the second order lambda calculus
• The theory of semi-functors
• Singleton, union and intersection types for program extraction
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Logic of refinement types