Imagen de Portada

Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Conoly, Owen, Erbsen, Andres, Chlipala, Adam
Formato:	Preprint
Publicado:	2025
Materias:	Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
por: Gross, Jason, et al.
Publicado: (2023)

Securing Cryptographic Software via Typed Assembly Language (Extended Version)
por: Song, Shixin, et al.
Publicado: (2025)

Accelerating Verified-Compiler Development with a Verified Rewriting Engine
por: Gross, Jason, et al.
Publicado: (2022)

Pyrosome: Verified Compilation for Modular Metatheory
por: Jamner, Dustin, et al.
Publicado: (2025)

The Jasmin Compiler Preserves Cryptographic Security
por: Arranz-Olmos, Santiago, et al.
Publicado: (2025)

Algorithmic Analysis of Termination Problems for Nondeterministic Quantum Programs
por: Fu, Jianling, et al.
Publicado: (2024)

Causality and Semantic Separation
por: Zhang, Anna, et al.
Publicado: (2026)

Partial Evaluation, Whole-Program Compilation
por: Fallin, Chris, et al.
Publicado: (2024)

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
por: Paraskevopoulou, Zoe
Publicado: (2026)

A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes
por: Różowski, Wojciech, et al.
Publicado: (2026)

Compilation Semantics for a Programming Language with Versions
por: Tanabe, Yudai, et al.
Publicado: (2023)

Hercules: A Compiler for Productive Programming of Heterogeneous Systems
por: Arbore, Russel, et al.
Publicado: (2025)

Compilation Quotient (CQ): A Metric for the Compilation Hardness of Programming Languages
por: Szabo, Violet, et al.
Publicado: (2024)

An Optimizing Just-In-Time Compiler for Rotor
por: Trindade, João H., et al.
Publicado: (2024)

Decompiling for Constant-Time Analysis
por: Arranz-Olmos, Santiago, et al.
Publicado: (2025)

A Proof-Producing Compiler for Blockchain Applications
por: Avigad, Jeremy, et al.
Publicado: (2025)

Bounded Exhaustive Random Program Generation for Testing Solidity Compilers
por: Ma, Haoyang, et al.
Publicado: (2025)

Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
por: Thibault, Jérémy, et al.
Publicado: (2025)

Compiler-Guided Inference-Time Adaptation: Improving GPT-5 Programming Performance in Idris
por: Li, Minda, et al.
Publicado: (2026)

Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs
por: Tekriwal, Mohit, et al.
Publicado: (2025)

DITRON: Distributed Multi-level Tiling Compiler for Parallel Tensor Programs
por: Zheng, Size, et al.
Publicado: (2026)

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
por: Wu, Jinhua, et al.
Publicado: (2025)

Symmetric Proofs of Parameterized Programs
por: Cheng, Ruotong, et al.
Publicado: (2026)

SECOMP: Formally Secure Compilation of Compartmentalized C Programs
por: Thibault, Jérémy, et al.
Publicado: (2024)

Compile-Time Java Stream Fusion via mapMulti
por: Bugayenko, Yegor, et al.
Publicado: (2026)

The CoCompiler: DSL Lifting via Relational Compilation
por: Spargo, Naomi, et al.
Publicado: (2025)

Grammar-Aware Literate Generative Mathematical Programming with Compiler-in-the-Loop
por: Rossi, Roberto, et al.
Publicado: (2026)

Linguine: A Natural-Language Programming Language with Formal Semantics and a Clean Compiler Pipeline
por: Hu, Lifan
Publicado: (2025)

Compiling with Arrays
por: Richter, David, et al.
Publicado: (2024)

AIOS Compiler: LLM as Interpreter for Natural Language Programming and Flow Programming of AI Agents
por: Xu, Shuyuan, et al.
Publicado: (2024)

Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
por: Nagy, Shaan, et al.
Publicado: (2024)

Quantitative Comparison of Credible Compilation and Verification In Coding Agent Compiler Development
por: Rinard, Martin
Publicado: (2026)

PolyBlocks: A Compiler Infrastructure for AI Chips and Programming Frameworks
por: Bondhugula, Uday, et al.
Publicado: (2026)

Pleasant Imperative Program Proofs with GallinaC
por: Fort, Frédéric, et al.
Publicado: (2025)

Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
por: Rinard, Martin
Publicado: (2026)

ASDF: A Compiler for Qwerty, a Basis-Oriented Quantum Programming Language
por: Adams, Austin J., et al.
Publicado: (2025)

MLIR-Smith: A Novel Random Program Generator for Evaluating Compiler Pipelines
por: Ates, Berke, et al.
Publicado: (2026)

CompilerGPT: Leveraging Large Language Models for Analyzing and Acting on Compiler Optimization Reports
por: Pirkelbauer, Peter, et al.
Publicado: (2025)

Secure Synthesis of Distributed Cryptographic Applications (Technical Report)
por: Acay, Coşku, et al.
Publicado: (2024)

Compilation as Multi-Language Semantics
por: Bowman, William J.
Publicado: (2025)