Realizability interpretation of generalized inductive definitions

DOI10.1016/0304-3975(94)90092-2MaRDI QIDQ1331920zbMATH OpenOpenAlexWikidataFDO

Authors 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

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

Recommendations

• TWO REALIZABILITY INTERPRETATIONS OF MONOTONE INDUCTIVE DEFINITIONS
• Monotone recursive definition of predicates and its realizability interpretation
• scientific article; zbMATH DE number 3557757
• Functional interpretation and inductive definitions

Cites work

• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 4006266 (Why is no real title available?)
• scientific article; zbMATH DE number 3687373 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 3556031 (Why is no real title available?)
• Constructive mathematics and computer programming
• Constructivism in mathematics. An introduction. Volume I
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Program synthesis using realizability

Cited in

(7)

• Monotone recursive definition of predicates and its realizability interpretation
• Realisability and adequacy for (co)induction
• A New Translation for Semi-classical Theories — Backtracking without CPS
• scientific article; zbMATH DE number 65538 (Why is no real title available?)
• Martin-Löf's type theory as an open-ended framework
• A convenient category of locally preordered spaces
• Generalized definitional reflection and the inversion principle

Describes a project that uses

Uses Software

• Nuprl

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1331920)