scientific article; zbMATH DE number 7471712
From MaRDI portal
Publication:5028480
Joshua Schneider, Dmitriy Traytel, Basil Fürer, Andreas Lochbihler
Publication date: 9 February 2022
Full work available at URL: https://arxiv.org/abs/2104.05348
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- From types to sets by local type definition in higher-order logic
- Relational parametricity and quotient preservation for modular (co)datatypes
- Almost event-rate independent monitoring
- CryptHOL: game-based proofs in higher-order logic
- Terminal coalgebras in well-founded set theory
- Automatic refinement to efficient data structures: a comparison of two approaches
- Types and coalgebraic structure
- Witnessing (Co)datatypes
- Equational Reasoning with Applicative Functors
- Cardinals in Isabelle/HOL
- Unified Decision Procedures for Regular Expression Equivalence
- Concrete Semantics
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Refinements for Free!
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
- Presentation of Set Functors: A Coalgebraic Perspective
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types
- Quotients of Bounded Natural Functors
- Defining functions on equivalence classes
- Mathematics of Program Construction
- Pragmatic Quotient Types in Coq
- Theorem Proving in Higher Order Logics
- Algebra and Coalgebra in Computer Science
- General Bindings and Alpha-Equivalence in Nominal Isabelle
- Effect polymorphism in higher-order logic (proof pearl)
- Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor.
This page was built for publication:
