About: Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations

Not logged in : Login

(Sponging disallowed)

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations Goto Sponge NotDistinct Permalink

An Entity of Type : bibo:BookSection, within Data Space : linkeddata.uriburner.com:28898 associated with source document(s)

Attributes	Values
type	http://eprints.org/ontology/BookSectionEPrint http://eprints.org/ontology/EPrint Article Book Section
seeAlso	HTML Summary of #66330 Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
sameAs	Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
http://eprints.org/ontology/hasAccepted	Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations (PDF)
http://eprints.org/ontology/hasDocument	Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations (Other) Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations (Other) Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations (Other) Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations (Other) Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations (Other) Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations (PDF)
dc:hasVersion	Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations (PDF)
Title	Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
described by	https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
Date	2018-01-08
Creator	Samuel Hym David Nowak Jean-Yves Moyen Micaela Mayero Hugo Férée
status	peer reviewed published
Publisher	ACM
abstract	We present a Coq library that allows for readily proving that a function is computable in polynomial time. It is based on quasi-interpretations that, in combination with termination ordering, provide a characterisation of the class FP of functions computable in polynomial time. At the heart of this formalisation is a proof of soundness and extensional completeness. Compared to the original paper proof, we had to fill a lot of not so trivial details that were left to the reader and fix a few glitches. To demonstrate the usability of our library, we apply it to the modular exponentiation.
Is Part Of	https://kar.kent.ac.uk/id/repository
Subject	QA Mathematics (inc Computing science)
list of authors	https://kar.kent.ac.uk/id/eprint/66330#authors
presented at	CPP 2018 - The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
is topic of	https://raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
is primary topic of	HTML Summary of #66330 Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations

Faceted Search & Find service v1.17_git144 as of Jul 26 2024

Alternative Linked Data Documents: iSPARQL | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 08.03.3331 as of Aug 25 2024, on Linux (x86_64-ubuntu_noble-linux-glibc2.38-64), Single-Server Edition (378 GB total memory, 15 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software