Realizability interpretation of generalized inductive definitions

DOI10.1016/0304-3975(94)90092-2zbMath0801.03022OpenAlexW2051829567WikidataQ127957012 ScholiaQ127957012MaRDI QIDQ1331920

Satoshi Kobayashi, Makoto Tatsuta

Publication date: 5 December 1994

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(94)90092-2

zbMATH Keywords

proof-as-programq-realizability interpretation of generalized inductive definitions

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (4)

Monotone recursive definition of predicates and its realizability interpretation ⋮ A New Translation for Semi-classical Theories — Backtracking without CPS ⋮ A convenient category of locally preordered spaces ⋮ MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK

Uses Software

• Nuprl

Cites Work

• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Program synthesis using realizability
• Constructivism in mathematics. An introduction. Volume I
• Constructive mathematics and computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Realizability interpretation of generalized inductive definitions