2015/12/06 by Jonathan Sterling, Sterling, Jonathan
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1512.01837
openalex publication_date 2015/12/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
At the heart of intuitionistic type theory lies an intuitive semantics called the "meaning explanations"; crucially, when meaning explanations are taken as definitive for type theory, the core notion is no longer "proof" but "verification". We'll explore how type theories of this sort arise naturally as enrichments of logical theories with further judgements, and contrast this with modern proof-theoretic type theories which interpret the judgements and proofs of logics, not their propositions and verifications.