Some Wellfounded Trees in UniMath

DOI10.1007/978-3-319-42432-3_2MaRDI QIDQ2819193zbMATH OpenOpenAlexFDO

Authors Benedikt Ahrens, Anders Mörtberg

Publication date 28 September 2016

Published in Mathematical Software – ICMS 2016 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-42432-3_2

zbMATH Keywords

proof assistantinitial algebrasinductive datatypesunivalent type theoryUniMath

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Type theory (03B38)

Recommendations

• Uniforming n-place functions on ds(alpha)
• scientific article; zbMATH DE number 6680130
• Some model theory for generalized trees
• Unification of kinded infinite trees
• Uniformization, choice functions and well orders in the class of trees
• Trees, ultrametric spaces and bases with uniform structure
• scientific article; zbMATH DE number 1990727
• Inducibility and universality for trees
• Types for Proofs and Programs
• Unions of random trees and applications

Cites work

• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 3458870 (Why is no real title available?)
• scientific article; zbMATH DE number 1216133 (Why is no real title available?)
• An experimental library of formalized mathematics based on the univalent foundations
• An introduction to small scale reflection in Coq
• Cubical type theory: a constructive interpretation of the univalence axiom
• Inductive types in homotopy type theory
• Non-wellfounded trees in homotopy type theory
• Substitution in non-wellfounded syntax with variable binding
• Univalent categories and the Rezk completion
• de Bruijn notation as a nested datatype

Cited in

(5)

• Unifying Sets and Programs via Dependent Types
• From signatures to monads in \textsf{UniMath}
• Types for Proofs and Programs
• Uniforming n-place functions on ds(alpha)
• Heterogeneous substitution systems revisited

Describes a project that uses

Uses Software

• cubicaltt
• UniMath
• Coq/SSReflect
• Coq

This page was built for publication: Some Wellfounded Trees in UniMath

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