Propositional functions and families of types

DOI10.1305/ndjfl/1093635159zbMath0694.03038OpenAlexW2035241416MaRDI QIDQ908912

Jan Smith

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

zbMATH Keywords

universeMartin-Löf's type theoryspecificationsintuitionism\(\forall \)-eliminationextended type theoryrecursion principle

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Second- and higher-order arithmetic and fragments (03F35)

Related Items (4)

Inductive families ⋮ Setoids and universes ⋮ Containers, monads and induction recursion ⋮ A general formulation of simultaneous inductive-recursive definitions in type theory

Uses Software

• Nuprl

This page was built for publication: Propositional functions and families of types