Coercive subtyping in type theory

DOI10.1007/3-540-63172-0_45MaRDI QIDQ4362923zbMATH OpenFDO

Authors Zhaohui Luo

Publication date 13 November 1997

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

Full work available at URL https://doi.org/10.1007/3-540-63172-0_45

zbMATH Keywords

coercive subtypingdependent type theoriessubsumption

Mathematics Subject Classification ID

Logic in computer science (03B70) Second- and higher-order arithmetic and fragments (03F35) General topics in the theory of software (68N01)

Recommendations

• Coercive subtyping
• Coercive subtyping: theory and implementation
• Coherence and Transitivity in Coercive Subtyping
• Coercion completion and conservativity in coercive subtyping

Cited in

(28)

• Transitivity in coercive subtyping
• Dependent types with subtyping and late-bound overloading
• Coercive subtyping: theory and implementation
• Coercive subtyping via mappings of reduction behaviour
• Coercive subtyping for the calculus of constructions (extended abstract)
• Proof assistants for natural language semantics
• Definitional extension in type theory
• Coherence and Transitivity in Coercive Subtyping
• A computational view of implicit coercions in type theory
• Subtyping, declaratively. An exercise in mixed induction and coinduction
• Subset Coercions in Coq
• Manifest Fields and Module Mechanisms in Intensional Type Theory
• Coercive subtyping
• Some algorithmic and proof-theoretical aspects of coercive subtyping
• scientific article; zbMATH DE number 2003159 (Why is no real title available?)
• Soundness of Coercion in the Calculus of Constructions
• Object-oriented concepts and proof rules: Formalization in type theory and implementation in Yarrow
• Nonuniform coercions via unification hints
• Implementing type theory in higher order constraint logic programming
• Automated Reasoning with Analytic Tableaux and Related Methods
• Types for Proofs and Programs
• Types for Proofs and Programs
• An implementation of LF with coercive subtyping and universes
• Coercion completion and conservativity in coercive subtyping
• Adjectival and adverbial modification: the view from modern type theories
• On subtyping in type theories with canonical objects
• A dependently-typed calculus of event telicity and culminativity
• Integrating coercion with subtyping and multiple dispatch

This page was built for publication: Coercive subtyping in type theory

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