Acyclicity and Finite Linear Extendability: a Formal and Constructive Equivalence.

Linear extension of partial orders emerged in the late 1920's. Its computer-oriented version, \emph{i.e.}, topological sorting of finite partial orders, arose in the late 1950's. However, those issues have not yet been considered from a viewpoint that is both formal and constructive; this paper discusses a few related claims formally proved with the constructive proof assistant Coq. For instance, it states that a given decidable binary relation is acyclic and equality is decidable on its domain \emph{iff} an irreflexive linear extension can be computed uniformly for any of its finite restriction. A detailed introduction and proofs written in plain English shall help readers who are not familiar with constructive issues or Coq formalism