Foundations of dependent interoperability (Q4577812): Difference between revisions

@@ Property / describes a project that uses @@
+Equations
@@ Property / describes a project that uses: Equations / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Scala
@@ Property / describes a project that uses: Scala / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Fiat
@@ Property / describes a project that uses: Fiat / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq/SSReflect
@@ Property / describes a project that uses: Coq/SSReflect / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HoTT
@@ Property / describes a project that uses: HoTT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+gradualizerDynamicSemantics
@@ Property / describes a project that uses: gradualizerDynamicSemantics / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Propositions as [Types]
@@ Property / cites work: Propositions as [Types] / rank @@
+Normal rank
@@ Property / cites work @@
+A theory of gradual effect systems
@@ Property / cites work: A theory of gradual effect systems / rank @@
+Normal rank
@@ Property / cites work @@
+Gradual type-and-effect systems
@@ Property / cites work: Gradual type-and-effect systems / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Q5417200
@@ Property / cites work: Q5417200 / rank @@
+Normal rank
@@ Property / cites work @@
+Isomorphisms of types in the presence of higher-order references (extended version)
+Normal rank
@@ Property / cites work @@
+Eliminating dependent pattern matching without K
@@ Property / cites work: Eliminating dependent pattern matching without K / rank @@
+Normal rank
@@ Property / cites work @@
+Refinements for Free!
@@ Property / cites work: Refinements for Free! / rank @@
+Normal rank
@@ Property / cites work @@
+A short survey of isomorphisms of types
@@ Property / cites work: A short survey of isomorphisms of types / rank @@
+Normal rank
@@ Property / cites work @@
+Transporting functions across ornaments
@@ Property / cites work: Transporting functions across ornaments / rank @@
+Normal rank
@@ Property / cites work @@
+Partial type equivalences for verified dependent interoperability
+Normal rank
@@ Property / cites work @@
+Fiat
@@ Property / cites work: Fiat / rank @@
+Normal rank
@@ Property / cites work @@
+Contracts for higher-order functions
@@ Property / cites work: Contracts for higher-order functions / rank @@
+Normal rank
@@ Property / cites work @@
+Abstracting gradual typing
@@ Property / cites work: Abstracting gradual typing / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075246
@@ Property / cites work: Q3075246 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3978973
@@ Property / cites work: Q3978973 / rank @@
+Normal rank
@@ Property / cites work @@
+Classical isomorphisms of types
@@ Property / cites work: Classical isomorphisms of types / rank @@
+Normal rank
@@ Property / cites work @@
+Gradual refinement types
@@ Property / cites work: Gradual refinement types / rank @@
+Normal rank
@@ Property / cites work @@
+Contextual isomorphisms
@@ Property / cites work: Contextual isomorphisms / rank @@
+Normal rank
@@ Property / cites work @@
+Operational semantics for multi-language programs
@@ Property / cites work: Operational semantics for multi-language programs / rank @@
+Normal rank
@@ Property / cites work @@
+Q4736399
@@ Property / cites work: Q4736399 / rank @@
+Normal rank
@@ Property / cites work @@
+Erasure and Polymorphism in Pure Type Systems
@@ Property / cites work: Erasure and Polymorphism in Pure Type Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q4673424
@@ Property / cites work: Q4673424 / rank @@
+Normal rank
@@ Property / cites work @@
+Manifest Contracts for Datatypes
@@ Property / cites work: Manifest Contracts for Datatypes / rank @@
+Normal rank
@@ Property / cites work @@
+Equations: A Dependent Pattern-Matching Compiler
@@ Property / cites work: Equations: A Dependent Pattern-Matching Compiler / rank @@
+Normal rank
@@ Property / cites work @@
+First-Class Type Classes
@@ Property / cites work: First-Class Type Classes / rank @@
+Normal rank
@@ Property / cites work @@
+From Proposition to Program
@@ Property / cites work: From Proposition to Program / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank
@@ Property / cites work @@
+Gradual Typing for Annotated Type Systems
@@ Property / cites work: Gradual Typing for Annotated Type Systems / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1017/s0956796818000011
+Normal rank
@@ Property / OpenAlex ID @@
+W2767557842
@@ Property / OpenAlex ID: W2767557842 / rank @@
+Normal rank