|
|
(26 intermediate revisions by 5 users not shown) |
Property / author | |
| | |
Property / author: Andreas Lochbihler / rank | |
| Normal rank
| |
| Property / author |
| | |
| Property / author: Andreas Lochbihler / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Matita / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Coq / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Isabelle/HOL / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Isabelle/ZF / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: HOL-Omega / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Paco / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: MiniAgda / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Stern-Brocot Tree / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: HOL / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Lean / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: CIRC / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: HOL Light / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Isabelle / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: ML / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Haskell / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Agda / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: HOL Zero / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Transfer / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Lifting / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: HOLCF / rank |
| | Normal rank |
| Property / describes a project that uses |
| | |
| Property / describes a project that uses: Archive Formal Proofs / rank |
| | Normal rank |
| Property / MaRDI profile type |
| | |
| Property / MaRDI profile type: MaRDI publication profile / rank |
| | Normal rank |
| Property / full work available at URL |
| | |
| Property / full work available at URL: https://doi.org/10.1007/978-3-662-54434-1_5 / rank |
| | Normal rank |
| Property / OpenAlex ID |
| | |
| Property / OpenAlex ID: W2595416494 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Containers: Constructing strictly positive types / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Compositional Coinduction with Sized Types / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Well-founded recursion with copatterns and sized types / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Copatterns / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The Matita Interactive Theorem Prover / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Productive coprogramming with guarded recursion / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Proofs for free / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Typed Lambda Calculi and Applications / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Inductive and Coinductive Components of Corecursive Functions in Coq / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Friends with Benefits / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Truly Modular (Co)datatypes for Isabelle/HOL / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Foundational extensible corecursion: a proof assistant perspective / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Witnessing (Co)datatypes / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A Brief Overview of Agda – A Functional Language with Dependent Types / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q5417200 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q3962450 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: FUNCTIONAL PEARLS: Probabilistic functional programming in Haskell / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Codifying guarded definitions with recursive schemes / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q5287513 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q3784044 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q3024873 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: HOL Light: An Overview / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The Bird Tree / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The HOL-Omega Logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The power of parameterization in coinductive proof / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Language Constructs for Non-Well-Founded Computation / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q4649560 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Fast Pattern Matching in Strings / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Partial Recursive Functions in Higher-Order Logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Automating Theorem Proving with SMT / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Probabilistic Functions and Cryptographic Oracles in Higher Order Logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Recursive Functions on Lazy Lists via Domains and Topologies / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: CIRC: A Behavioral Verification Tool Based on Circular Coinduction / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Completely iterative algebras and completely iterative monads / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Abstract GSOS Rules and a Modular Treatment of Recursive Definitions / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Parametric corecursion / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: The Lean Theorem Prover (System Description) / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Isabelle/HOL. A proof assistant for higher-order logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A fixedpoint approach to implementing (Co)inductive definitions / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Mechanizing coinduction and corecursion in higher-order logic / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Coinduction All the Way Up / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Coalgebraic Bisimulation-Up-To / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Q4251915 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A Brief Overview of HOL4 / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Indexed codata types / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Formal Languages, Formally and Coinductively / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving / rank |
| | Normal rank |
| Property / cites work |
| | |
| Property / cites work: A note on model checking the modal \(\nu\)-calculus / rank |
| | Normal rank |
links / mardi / name | links / mardi / name |
| | |