Propositional functions and families of types
From MaRDI portal
Publication:908912
DOI10.1305/ndjfl/1093635159zbMath0694.03038MaRDI QIDQ908912
Publication date: 1989
Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1305/ndjfl/1093635159
universe; Martin-Löf's type theory; specifications; intuitionism; \(\forall \)-elimination; extended type theory; recursion principle
68Q60: Specification and verification (program logics, model checking, etc.)
68Q65: Abstract data types; algebraic specification
03F35: Second- and higher-order arithmetic and fragments
Related Items
A general formulation of simultaneous inductive-recursive definitions in type theory, Containers, monads and induction recursion, Inductive families, Setoids and universes
Uses Software