Foundations of dependent interoperability

DOI10.1017/S0956796818000011MaRDI QIDQ4577812zbMATH OpenOpenAlexWikidataFDO

Authors Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter

Publication date 3 August 2018

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0956796818000011

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• Partial type equivalences for verified dependent interoperability
• scientific article; zbMATH DE number 1497808
• Ynot: dependent types for imperative programs
• Constructive Galois connections
• Self-certification: bootstrapping certified typecheckers in F^ with Coq

Cites work

• scientific article; zbMATH DE number 19486 (Why is no real title available?)
• scientific article; zbMATH DE number 2163037 (Why is no real title available?)
• scientific article; zbMATH DE number 2085175 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• A short survey of isomorphisms of types
• A theory of gradual effect systems
• Abstracting gradual typing
• An introduction to small scale reflection in Coq
• Classical isomorphisms of types
• Contextual isomorphisms
• Contracts for higher-order functions
• Eliminating dependent pattern matching without K
• Equations: a dependent pattern-matching compiler
• Erasure and Polymorphism in Pure Type Systems
• Fiat: deductive synthesis of abstract data types in a proof assistant
• First-Class Type Classes
• From proposition to program. Embedding the refinement calculus in Coq
• Gradual Typing for Annotated Type Systems
• Gradual refinement types
• Gradual type-and-effect systems
• Homotopy type theory. Univalent foundations of mathematics
• Isomorphisms of types in the presence of higher-order references
• Manifest contracts for datatypes
• Operational semantics for multi-language programs
• Partial type equivalences for verified dependent interoperability
• Propositions as [Types]
• Refinements for free!
• Transporting functions across ornaments
• Types for Proofs and Programs

Cited in

(3)

• Gradual type theory
• ANF preserves dependent types up to extensional equality
• Call-by-name gradual type theory

Describes a project that uses

Uses Software

• Equations
• gradualizerDynamicSemantics
• Fiat
• HoTT
• Coq/SSReflect
• Scala
• Coq

This page was built for publication: Foundations of dependent interoperability

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