Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs

DOI10.1007/s10817-019-09530-2zbMath1468.68057OpenAlexW3165217919WikidataQ113901242 ScholiaQ113901242MaRDI QIDQ2331068

Ugo Dal Lago, Gilles Barthe, Patrick Baillot

Publication date: 25 October 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-019-09530-2

zbMATH Keywords

complexity analysisimplicit computational complexitycryptographic proofslinear dependent types

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Cryptography (94A60) Functional programming and lambda calculus (68N18) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items (1)

Read/write factorizable programs

Uses Software

• COSTA
• EasyCrypt
• F*

Cites Work

• Unnamed Item
• Light types for polynomial time computation in lambda calculus
• Safe recursion with higher types and BCK-algebra
• Dependent types for program termination verification
• (Leftmost-Outermost) Beta Reduction is Invariant, Indeed
• Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
• The geometry of types
• The geometry of linear higher-order recursion
• A flow calculus of mwp -bounds for complexity analysis
• Lightweight semiformal time complexity analysis for purely functional data structures
• Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
• Amortized Resource Analysis with Polynomial Potential
• On Expected Probabilistic Polynomial-Time Adversaries: A Suggestion for Restricted Definitions and Their Benefits
• Linear Dependent Types and Relative Completeness
• Secure distributed programming with value-dependent types
• Cost recurrences for DML programs
• Computer-Aided Security Proofs for the Working Cryptographer
• Formal certification of code-based cryptographic proofs
• SPEED
• Probabilistic relational verification for cryptographic implementations

This page was built for publication: Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs