Types for Proofs and Programs

DOI10.1007/b98246zbMath1100.03518OpenAlexW4298423642MaRDI QIDQ5712319

Hongwei Xi

Publication date: 23 December 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b98246

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Dependently typed array programs don't go wrong ⋮ Polymorphic typed defunctionalization and concretization ⋮ Size-based termination of higher-order rewriting ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Unnamed Item ⋮ A Classical Realizability Model for a Semantical Value Restriction ⋮ Session Types with Arithmetic Refinements ⋮ Type-level Computation Using Narrowing in Ωmega