Sciweavers

Share
ITP
2010
141views Mathematics» more  ITP 2010»
8 years 4 months ago
(Nominal) Unification by Recursive Descent with Triangular Substitutions
Using HOL4, we mechanise termination and correctness for two unification algorithms, written in a recursive descent style. One computes unifiers for first order terms, the other fo...
Ramana Kumar, Michael Norrish
ITP
2010
155views Mathematics» more  ITP 2010»
8 years 4 months ago
Translation in XBRL standardization
eXtensible Business Reporting Language (XBRL) presents new opportunities for integrating information flow within communities of diverse organisations thereby significantly enhanci...
Indrit Troshani, Andy Lymer
ITP
2010
172views Mathematics» more  ITP 2010»
8 years 4 months ago
Automated Machine-Checked Hybrid System Safety Proofs
mentation of the Abstraction Method In Coq Eelis van der Weegen Institute for Computing and Information Sciences Raboud University Nijmegen This technical report documents our deve...
Herman Geuvers, Adam Koprowski, Dan Synek, Eelis v...
ITP
2010
152views Mathematics» more  ITP 2010»
8 years 4 months ago
Higher-Order Abstract Syntax in Isabelle/HOL
rder Abstract Syntax in Isabelle/HOL Douglas J. Howe Carleton University July 13, 2010 Douglas J. Howe (Carleton University) HOAS in Isabelle/HOL July 13, 2010 1 / 8
Douglas J. Howe
ITP
2010
143views Mathematics» more  ITP 2010»
8 years 8 months ago
A Certified Denotational Abstract Interpreter
ied Denotational Abstract Interpreter (Proof Pearl) David Cachera1 and David Pichardie2 1 IRISA / ENS Cachan (Bretagne), France 2 INRIA Rennes
David Cachera, David Pichardie
ITP
2010
143views Mathematics» more  ITP 2010»
8 years 8 months ago
Formal Study of Plane Delaunay Triangulation
Jean-François Dufourd, Yves Bertot
ITP
2010
109views Mathematics» more  ITP 2010»
8 years 8 months ago
A Tactic Language for Declarative Proofs
Influenced by the success of the MIZAR system many declarative proof languages have been developed in the theorem prover community, as declarative proofs are more readable, easier...
Serge Autexier, Dominik Dietrich
books