Imagen de Portada

Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Knothe, David, Bringmann, Oliver
Formato:	Preprint
Publicado:	2026
Materias:	Programming Languages Logic in Computer Science F.3.2; D.3.4; D.2.4
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Verified VCG and Verified Compiler for Dafny
por: Nezamabadi, Daniel, et al.
Publicado: (2025)

The Denotational Semantics of SSA
por: Ghalayini, Jad Elkhaleq, et al.
Publicado: (2024)

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

Baking for Dafny: A CakeML Backend for Dafny
por: Nezamabadi, Daniel, et al.
Publicado: (2025)

Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
por: Zaiser, Fabian, et al.
Publicado: (2024)

Scott's Representation Theorem and the Univalent Karoubi Envelope
por: van der Leer, Arnoud, et al.
Publicado: (2025)

Linear-Time Graph Programs without Preconditions
por: Alaoui, Ziad Ismaili, et al.
Publicado: (2025)

Sharing Analysis in the Pawns Compiler
por: Naish, Lee
Publicado: (2024)

Complete Fusion for Stateful Streams: Equational Theory of Stateful Streams and Fusion as Normalization-by-Evaluation
por: Kiselyov, Oleg, et al.
Publicado: (2024)

TensorRight: Automated Verification of Tensor Graph Rewrites
por: Arora, Jai, et al.
Publicado: (2025)

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
por: Frenkel, Eden, et al.
Publicado: (2026)

A New Interaction Concept for Interactive and Autoactive Program Verification
por: Pfeifer, Wolfram, et al.
Publicado: (2026)

Model Checking Probabilistic Operator Precedence Automata
por: Pontiggia, Francesco, et al.
Publicado: (2024)

Closure Conversion, Flat Environments, and the Complexity of Abstract Machines
por: Accattoli, Beniamino, et al.
Publicado: (2025)

Quantitative Assurance and Synthesis of Controllers from Activity Diagrams
por: Ye, Kangfeng, et al.
Publicado: (2024)

Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types
por: Suwa, Takashi, et al.
Publicado: (2026)

Genericity Through Stratification
por: Arrial, Victor, et al.
Publicado: (2024)

AdapTT: Functoriality for Dependent Type Casts
por: Adjedj, Arthur, et al.
Publicado: (2025)

Meta-Monomorphizing Specializations
por: Bruzzone, Federico, et al.
Publicado: (2026)

Prioritizing Configuration Relevance via Compiler-Based Refined Feature Ranking
por: Bruzzone, Federico, et al.
Publicado: (2026)

Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Version)
por: Sextl, Florian, et al.
Publicado: (2023)

Formally Modelling the Rijkswaterstaat Tunnel Control Systems in a Constrained Industrial Environment
por: Jilissen, Kevin H. J., et al.
Publicado: (2024)

Definitional Functoriality for Dependent (Sub)Types -- Extended version
por: Laurent, Théo, et al.
Publicado: (2023)

Grounded Language Design for Lightweight Diagramming for Formal Methods
por: Prasad, Siddhartha, et al.
Publicado: (2024)

Context-Dependent Effects and Concurrency in Guarded Interaction Trees
por: Stepanenko, Sergei, et al.
Publicado: (2025)

Uniqueness is Separation
por: O'Connor, Liam, et al.
Publicado: (2026)

What does it take to certify a conversion checker?
por: Lennon-Bertrand, Meven
Publicado: (2025)

Verifying Device Drivers with Pancake
por: Zhao, Junming, et al.
Publicado: (2025)

Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
por: McCann, Alan L.
Publicado: (2026)

A Gentle Overview of Asynchronous Session-based Concurrency: Deadlock Freedom by Typing
por: Heuvel, Bas van den, et al.
Publicado: (2024)

Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries
por: McCann, Alan L.
Publicado: (2026)

Explicit Weakening
por: Wadler, Philip
Publicado: (2024)

Quantitative Verification with Neural Networks
por: Abate, Alessandro, et al.
Publicado: (2023)

Teaching Introductory Functional Programming Using Haskelite
por: Vasconcelos, Pedro
Publicado: (2025)

Space-time process algebra with asynchronous communication
por: Bergstra, J. A., et al.
Publicado: (2024)

A Graded Modal Type Theory for Pulse Schedules
por: Adams, Robin, et al.
Publicado: (2025)

Denotational Semantics for ODRL: Knowledge-Based Constraint Conflict Detection
por: Mustafa, Daham, et al.
Publicado: (2026)

From Separate Compilation to Sound Language Composition
por: Bruzzone, Federico, et al.
Publicado: (2026)

Verification of E-Voting Algorithms in Dafny
por: Büttner, Robert, et al.
Publicado: (2025)

SMT-based Symbolic Model-Checking for Operator Precedence Languages
por: Chiari, Michele, et al.
Publicado: (2024)