Applied type system (extended abstract)

DOI10.1007/978-3-540-24849-1_25MaRDI QIDQ5712319zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Pure type systems with subtyping. (Extended abstract)
• scientific article; zbMATH DE number 559219
• Combining programming with theorem proving
• ATS/LF: A type system for constructing proofs as total functional programs
• Dependent ML An approach to practical programming with dependent types

Cited in

(10)

• A Classical Realizability Model for a Semantical Value Restriction
• Type-level computation using narrowing in \(\Omega\)mega
• Combining programming with theorem proving
• Size-based termination of higher-order rewriting
• Introduction to generalized type systems
• Session Types with Arithmetic Refinements
• POPLMark reloaded: mechanizing proofs by logical relations
• PML2: integrated program verification in ML
• Dependently typed array programs don't go wrong
• Polymorphic typed defunctionalization and concretization

This page was built for publication: Applied type system (extended abstract)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5712319)