Formal study of functional orbits in finite domains

DOI10.1016/J.TCS.2014.10.041MaRDI QIDQ483296zbMATH OpenOpenAlexFDO

Authors Jean-François Dufourd

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

zbMATH Keywords

program correctnessformal specificationCoq systemalgebraic data typecomputer-aided prooffunctional orbitslinked representationmemory shape analysis

Mathematics Subject Classification ID

Computer graphics; computational geometry (digital and algorithmic aspects) (68U05) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Recommendations

• Finite orbits for rational functions
• Finite polynomial orbits in finitely generated domains
• Integral orbits over function fields
• scientific article; zbMATH DE number 1522545
• Formal functions on prevalued domains
• Orbits of automorphisms of integral domains
• Orbits and continuity of certain class of functions
• Integrality estimates in orbits over function fields
• Coverage, invariability and orbits by structural functions
• Functions and functional on finite systems

Cites work

• scientific article; zbMATH DE number 1612488 (Why is no real title available?)
• scientific article; zbMATH DE number 3489159 (Why is no real title available?)
• scientific article; zbMATH DE number 3495348 (Why is no real title available?)
• scientific article; zbMATH DE number 3518832 (Why is no real title available?)
• scientific article; zbMATH DE number 3585754 (Why is no real title available?)
• scientific article; zbMATH DE number 3303654 (Why is no real title available?)
• scientific article; zbMATH DE number 3303655 (Why is no real title available?)
• scientific article; zbMATH DE number 3410595 (Why is no real title available?)
• A Theorem on Boolean Matrices
• An axiomatic basis for computer programming
• An efficient machine-independent procedure for garbage collection in various list structures
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• Design and formal proof of a new optimal image segmentation program with hypermaps
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• Formal proof - the four color theorem
• Formal study of plane Delaunay triangulation
• Functional specification and prototyping with oriented combinatorial maps
• Generalised multi-pattern-based verification of programs with linear linked structures
• Hypermap specification and certified linked implementation using orbits
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Iterated function systems and the global construction of fractals
• N-DIMENSIONAL GENERALIZED COMBINATORIAL MAPS AND CELLULAR QUASI-MANIFOLDS
• Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
• Proving pointer programs in higher-order logic
• Region-based shape analysis with tracked locations
• Rotors in Graph Theory
• Shape Analysis for Composite Data Structures

Cited in

(2)

• Simpler proofs with decentralized invariants
• Analysing the dynamics of digital chaotic maps via a new period search algorithm

Describes a project that uses

Uses Software

• CGoGN
• CATIA V5
• Coq
• CGAL

This page was built for publication: Formal study of functional orbits in finite domains

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q483296)