scientific article; zbMATH DE number 7471719

MaRDI QIDQ5028488

Jérémy Dubut, Akihisa Yamada

Publication date: 9 February 2022

Full work available at URL: https://arxiv.org/abs/2009.13065

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

lattice theoryfixed-pointsorder theoryIsabelle/HO

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Uses Software

• Coq
• Nitpick
• Isabelle/HOL
• PIDE
• Isabelle/jEdit
• HOL Light
• Sledgehammer
• Agda
• seL4

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Chain-complete posets and directed sets with applications
• Isabelle/HOL. A proof assistant for higher-order logic
• Trellis theory
• The method of successive approximations for functional equations
• Sur le théorème de Zorn
• A lattice-theoretical fixpoint theorem and its applications
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• A Brief Overview of Agda – A Functional Language with Dependent Types
• A Theorem on Partially Ordered Sets, With Applications to Fixed Point Theorems
• Weak chain-completeness and fixed point property for pseudo-ordered sets
• Grammar Analysis and Parsing by Abstract Interpretation
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• Fixed points and common fixed points theorems in pseudo-ordered sets
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
• Sledgehammer: Judgement Day
• Interpretation of Locales in Isabelle: Theories and Proof Contexts

This page was built for publication: