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

inductive datatypesinitial algebrasproof assistantUniMathunivalent type theory

Mathematics Subject Classification ID

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

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

• 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
• de Bruijn notation as a nested datatype
• 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?)
• 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

Cited in

(5)

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

Describes a project that uses

Uses Software

• Coq/SSReflect
• Coq
• UniMath
• cubicaltt

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)