Coercive subtyping

DOI10.1093/LOGCOM/9.1.105zbMATH Open0920.03062OpenAlexW4243054153MaRDI QIDQ4238487FDOQ4238487

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

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

zbMATH Keywords

type theorylogical frameworkcoercive subtypingcomputer-assisted formal reasoning

Mathematics Subject Classification ID

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

Cited In (32)

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

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)