A formalization of polytime functions

DOI10.1007/978-3-642-22863-6_11MaRDI QIDQ3088001zbMATH OpenOpenAlexFDO

Authors Sylvain Heraud, David Nowak

Publication date 17 August 2011

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-22863-6_11

zbMATH Keywords

cryptographyimplicit computational complexity

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Cryptography (94A60)

Recommendations

• Polytime, combinatory logic and positive safe induction
• A new recursion-theoretic characterization of the polytime functions
• scientific article; zbMATH DE number 445159
• A foundational delineation of poly-time
• Function algebraic characterizations of the polytime functions

Cites work

• scientific article; zbMATH DE number 3922632 (Why is no real title available?)
• A Calculus for Game-Based Security Proofs
• A Formal Language for Cryptographic Pseudocode
• A new function algebra of EXPTIME functions by safe nested recursion
• A new recursion-theoretic characterization of the polytime functions
• Complexity Analysis by Rewriting
• Computer Science Logic
• Formal certification of code-based cryptographic proofs
• New directions in cryptography
• Safe recursion with higher types and BCK-algebra
• The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs
• The computational SLR: a logic for reasoning about computational indistinguishability
• Theorem Proving in Higher Order Logics

Cited in

(3)

• A formal definition of time in LOTOS
• Formal security proofs with minimal fuss: implicit computational complexity at work
• scientific article; zbMATH DE number 1543364 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A formalization of polytime functions

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