Programming up to congruence

DOI10.1145/2676726.2676974MaRDI QIDQ2819823zbMATH OpenOpenAlexFDO

Authors Vilhelm Sjöberg, Stephanie Weirich

Publication date 29 September 2016

Published in Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2676726.2676974

zbMATH Keywords

congruence closuredependent types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Dependent types and program equivalence
• Congruence closure in intensional type theory
• : dependent types without the sugar
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Combining proofs and programs in a dependently typed language

Cited in

(6)

• Congruence closure in intensional type theory
• Unified syntax with iso-types
• A cubical language for Bishop sets
• Dependent types and program equivalence
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
• Congruence closure modulo groups

This page was built for publication: Programming up to congruence

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