Cover Image

Formalising Inductive and Coinductive Containers

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Damato, Stefania, Altenkirch, Thorsten, Ljungström, Axel
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science Logic
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Distributive Laws of Monadic Containers
by: Purdy, Chris, et al.
Published: (2025)

Formalising and Computing the Fourth Homotopy Group of the $3$-Sphere in Cubical Agda
by: Ljungström, Axel, et al.
Published: (2023)

Symmetric Monoidal Smash Products in Homotopy Type Theory
by: Ljungström, Axel
Published: (2024)

The Size-Change Principle for Mixed Inductive and Coinductive types
by: Hyvernat, Pierre
Published: (2024)

Master Thesis Impredicative Encodings of Inductive and Coinductive Types
by: Bronsveld, Steven, et al.
Published: (2025)

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory
by: de Jong, Tom, et al.
Published: (2026)

Substitution Without Copy and Paste
by: Altenkirch, Thorsten, et al.
Published: (2025)

The Groupoid-Syntax of Type Theory is a Set
by: Altenkirch, Thorsten, et al.
Published: (2025)

Synthetic 1-Categories in Directed Type Theory
by: Altenkirch, Thorsten, et al.
Published: (2024)

Computational Synthetic Cohomology Theory in Homotopy Type Theory
by: Ljungström, Axel, et al.
Published: (2024)

The Steenrod squares via unordered joins
by: Ljungström, Axel, et al.
Published: (2025)

Logics and Type Theory: essays dedicated to Stefano Berardi on the occasion of his 1000000th birthday
by: Altenkirch, Thorsten, et al.
Published: (2026)

Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions
by: Stoltenow, Lara, et al.
Published: (2024)

Coinductive Proofs for Temporal Hyperliveness
by: Correnson, Arthur, et al.
Published: (2025)

Coinductive Streams in Monoidal Categories
by: Di Lavore, Elena, et al.
Published: (2022)

A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity
by: Grabmayer, Clemens
Published: (2022)

$Π_{2}$-Rule Systems and Inductive Classes of Gödel Algebras
by: Almeida, Rodrigo Nicolau
Published: (2023)

Formalising the Double-Pushout Approach to Graph Transformation
by: Söldner, Robert, et al.
Published: (2023)

Compression for Coinductive Infinitary Rewriting: A Generic Approach, with Applications to Cut-Elimination for Non-Wellfounded Proofs
by: Cerda, Rémy, et al.
Published: (2025)

Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic
by: Santo, José Espírito, et al.
Published: (2020)

Impredicative Encodings of (Higher) Inductive Types
by: Awodey, Steve, et al.
Published: (2018)

Topological Semantics for Common Inductive Knowledge
by: Namachivayam, Siddharth
Published: (2026)

Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
by: Kolesar, John, et al.
Published: (2025)

Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics
by: Ambridge, Todd Waugh
Published: (2024)

Formalising the Bruhat-Tits Tree
by: Ludwig, Judith, et al.
Published: (2025)

Initial Algebras of Domains via Quotient Inductive-Inductive Types
by: van Collem, Simcha, et al.
Published: (2025)

Coinductive well-foundedness
by: Petrakis, Iosif
Published: (2025)

Formalising the local compactness of the adele ring
by: Mercuri, Salvatore
Published: (2024)

Rewriting and Inductive Reasoning
by: Hajdu, Márton, et al.
Published: (2024)

Equational and Inductive Reasoning for Maude in Athena
by: Sanabria, Mateo, et al.
Published: (2026)

Property Checking Without Inductive Invariants
by: Goldberg, Eugene
Published: (2016)

Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance
by: Reimann, Jesse, et al.
Published: (2024)

A Logical Formalisation of a Hypothesis in Weighted Abduction: towards User-Feedback Dialogues
by: Motoura, Shota, et al.
Published: (2025)

FRETting about Requirements: Formalised Requirements for an Aircraft Engine Controller
by: Farrell, Marie, et al.
Published: (2021)

Totality for Mixed Inductive and Coinductive Types
by: Hyvernat, Pierre
Published: (2019)

Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation
by: Bertrand, Meven Lennon, et al.
Published: (2026)

Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
by: Su, Wanyun, et al.
Published: (2024)

An Abstract Account of Up-to Techniques for Inductive Behavioural Relations
by: Sangiorgi, Davide
Published: (2024)

Compositional Inductive Invariant Inference via Assume-Guarantee Reasoning
by: Dardik, Ian, et al.
Published: (2025)

Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols
by: Ratschan, Stefan, et al.
Published: (2026)