Coercive subtyping

DOI10.1093/LOGCOM/9.1.105MaRDI QIDQ4238487zbMATH OpenOpenAlexFDO

Authors Zhaohui Luo

Publication date 30 March 1999

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/082432bdb9cc0abb8c554c0ba2cae862ccc48fa9

zbMATH Keywords

coercive subtypingcomputer-assisted formal reasoninglogical frameworktype theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Second- and higher-order arithmetic and fragments (03F35) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1086673
• Coercive subtyping: theory and implementation
• Coherence and Transitivity in Coercive Subtyping
• Coercion completion and conservativity in coercive subtyping

Cited in

(38)

• A constructive algebraic hierarchy in Coq.
• Transitivity in coercive subtyping
• Coercive subtyping: theory and implementation
• Natural language inference in Coq
• User interaction with the Matita proof assistant
• Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
• Coercive subtyping via mappings of reduction behaviour
• Typed compilation of inclusive subtyping
• Definitional extension in type theory
• Hints in Unification
• A computational view of implicit coercions in type theory
• Working with Mathematical Structures in Type Theory
• Coercions in a polymorphic type system
• Structural subtyping for inductive types with functorial equality rules
• Subtyping, declaratively. An exercise in mixed induction and coinduction
• Manifest Fields and Module Mechanisms in Intensional Type Theory
• scientific article; zbMATH DE number 1301735 (Why is no real title available?)
• scientific article; zbMATH DE number 1086673 (Why is no real title available?)
• scientific article; zbMATH DE number 2003159 (Why is no real title available?)
• scientific article; zbMATH DE number 1497808 (Why is no real title available?)
• Logical relations for coherence of effect subtyping
• Implicit coercions in type systems
• Taming the merge operator
• A user interface for a mathematical system that allows ambiguous formulae
• The Matita interactive theorem prover
• Logical relations for coherence of effect subtyping
• Automated Reasoning with Analytic Tableaux and Related Methods
• Types for Proofs and Programs
• 2-Dimensional Directed Type Theory
• Coercion completion and conservativity in coercive subtyping
• Subtyping dependent types
• Propositional forms of judgemental interpretations
• Gradability in MTT-Semantics
• Adjectival and adverbial modification: the view from modern type theories
• On subtyping in type theories with canonical objects
• Categorical models of subtyping
• A dependently-typed calculus of event telicity and culminativity
• Subtype universes

This page was built for publication: Coercive subtyping

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