Partial type equivalences for verified dependent interoperability

DOI10.1145/2951913.2951933zbMATH Open1360.68322OpenAlexW2413556709MaRDI QIDQ2985778FDOQ2985778

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

Publication date: 10 May 2017

Published in: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01328012/file/main.pdf

Recommendations

• An extensible equality checking algorithm for dependent type theories
• Dependent types and program equivalence
• Dependent types ensure partial correctness of theorem provers
• Dependent types and formal synthesis
• Extensional equality preservation and verified generic programming
• Efficient Verified Programs in a Type Theory with Mixed Constructivity

zbMATH Keywords

dependent typesinteroperabilitytype equivalences

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18)

Cited In (4)

• Title not available (Why is that?)
• Type-Based Verification of Correspondence Assertions for Communication Protocols
• ANF preserves dependent types up to extensional equality
• Foundations of dependent interoperability

Uses Software

• Coq
• OCaml

This page was built for publication: Partial type equivalences for verified dependent interoperability

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