Formal polytypic programs and proofs

DOI10.1017/S0956796810000158MaRDI QIDQ3070767zbMATH OpenFDO

Authors Wendy Verbruggen, Edsko Devries, Arthur Hughes

Publication date 26 January 2011

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

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

zbMATH Keywords

Coqpolytypic functions

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 1424014
• Applications of polytypism in theorem proving
• Polytypic programming in Maude
• Implementation of Functional Languages
• Towards Generic Programming with Sized Types

Cites work

• A UNIVERSE OF STRICTLY POSITIVE FAMILIES
• Boxy types, inference for higher-rank types and impredicativity
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Complete and decidable type inference for GADTs
• Container types categorically
• Derivable type classes
• Generic programming in 3D
• Generics for the masses
• Inductive and coinductive components of corecursive functions in Coq
• Type checking with universes
• Type-based termination of generic programs

Cited in

(7)

• Polytypic programming in Maude
• Applications of polytypism in theorem proving
• Towards Generic Programming with Sized Types
• scientific article; zbMATH DE number 1424014 (Why is no real title available?)
• Extensional equality preservation and verified generic programming
• Programming Languages and Systems
• Theorem Proving in Higher Order Logics

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Formal polytypic programs and proofs

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