Formal study of functional orbits in finite domains
From MaRDI portal
Publication:483296
DOI10.1016/j.tcs.2014.10.041zbMath1317.68208OpenAlexW2085828618MaRDI QIDQ483296
Publication date: 16 December 2014
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2014.10.041
formal specificationprogram correctnessCoq systemalgebraic data typecomputer-aided prooffunctional orbitslinked representationmemory shape analysis
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
Simpler proofs with decentralized invariants ⋮ Analysing the dynamics of digital chaotic maps via a new period search algorithm
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Designing and proving correct a convex hull algorithm with hypermaps in Coq
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
- Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
- Functional specification and prototyping with oriented combinatorial maps
- Proving pointer programs in higher-order logic
- Generalised multi-pattern-based verification of programs with linear linked structures
- Design and formal proof of a new optimal image segmentation program with hypermaps
- Hypermap Specification and Certified Linked Implementation Using Orbits
- Iterated function systems and the global construction of fractals
- Rotors in Graph Theory
- N-DIMENSIONAL GENERALIZED COMBINATORIAL MAPS AND CELLULAR QUASI-MANIFOLDS
- Region-based shape analysis with tracked locations
- Shape Analysis for Composite Data Structures
- An efficient machine-independent procedure for garbage collection in various list structures
- An axiomatic basis for computer programming
- A Theorem on Boolean Matrices
- Formal Study of Plane Delaunay Triangulation
This page was built for publication: Formal study of functional orbits in finite domains
