Formal study of functional orbits in finite domains
type: Item
instance of: scholarly article
title: Formal study of functional orbits in finite domains
zbMATH Open document ID: 1317.68208
author: Jean-François Dufourd
published in: Theoretical Computer Science
publication date: 2014-12-16T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68U05
zbMATH DE Number: 6380850
zbMATH Keywords: formal specification
zbMATH Keywords: functional orbits
zbMATH Keywords: program correctness
zbMATH Keywords: linked representation
zbMATH Keywords: algebraic data type
zbMATH Keywords: memory shape analysis
zbMATH Keywords: computer-aided proof
zbMATH Keywords: Coq system
describes a project that uses: CGAL
describes a project that uses: Coq
describes a project that uses: CATIA V5
describes a project that uses: CGoGN
MaRDI profile type: Publication
full work available at URL: j.tcs.2014.10.041
OpenAlex ID: W2085828618
cites work: Iterated function systems and the global construction of fractals
cites work: Shape Analysis for Composite Data Structures
cites work: Q4096964
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Q2721096
cites work: Designing and proving correct a convex hull algorithm with hypermaps in Coq
cites work: Q5674963
cites work: Generalised multi-pattern-based verification of programs with linear linked structures
cites work: Q4071773
cites work: Design and formal proof of a new optimal image segmentation program with hypermaps
cites work: Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
cites work: An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
cites work: Hypermap Specification and Certified Linked Implementation Using Orbits
cites work: Formal Study of Plane Delaunay Triangulation
cites work: Functional specification and prototyping with oriented combinatorial maps
cites work: Q5302559
cites work: Q4077223
cites work: Region-based shape analysis with tracked locations
cites work: An axiomatic basis for computer programming
cites work: Q5585020
cites work: Q5585021
cites work: N-DIMENSIONAL GENERALIZED COMBINATORIAL MAPS AND CELLULAR QUASI-MANIFOLDS
cites work: Proving pointer programs in higher-order logic
cites work: Q4154814
cites work: An efficient machine-independent procedure for garbage collection in various list structures
cites work: Rotors in Graph Theory
cites work: A Theorem on Boolean Matrices
DOI: 10.1016/J.TCS.2014.10.041
Recommended article: Finite orbits for rational functions
Recommended article: Finite polynomial orbits in finitely generated domains
Recommended article: Integral orbits over function fields
Recommended article: Q4510780
Recommended article: Formal functions on prevalued domains
Recommended article: Orbits of automorphisms of integral domains
Recommended article: Q5324098
Recommended article: Integrality estimates in orbits over function fields
Recommended article: Coverage, invariability and orbits by structural functions
Recommended article: Functions and functional on finite systems
description: scientific article; zbMATH DE number 6380850