Inductive construction of repletion

DOI10.1023/A:1008604622568zbMath0933.03032MaRDI QIDQ1306716

Thomas Streicher

Publication date: 1999

Published in: Applied Categorical Structures (Search for Journal in Brave)

zbMATH Keywords

constructive type theorydenotational semanticsconstructive logicsynthetic domain theoryinductive definitionspredomainrepletion

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Categorical logic, topoi (03G30) Metamathematics of constructive systems (03F50)

Related Items

Observationally-induced Effect Monads: Upper and Lower Powerspace Constructions, Axioms and (counter)examples in synthetic domain theory