:: Library Catalog

Imagen de Portada

Guardado en:

Detalles Bibliográficos
Autores principales:	Fasse, Justus, Jacobs, Bart
Formato:	Preprint
Publicado:	2023
Materias:	Programming Languages Logic in Computer Science
Acceso en línea:	https://arxiv.org/abs/2312.15379
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

An approach for modularly verifying the core of Rust's atomic reference counting algorithm against the (Y)C20 memory consistency model
por: Jacobs, Bart, et al.
Publicado: (2025)

Towards a Coq-verified Chain of Esterel Semantics
por: Berry, Gérard, et al.
Publicado: (2019)

VeriFast's separation logic: a logic without laters for modular verification of fine-grained concurrent programs
por: Jacobs, Bart
Publicado: (2025)

A formal specification of the jq language
por: Färber, Michael
Publicado: (2024)

Kleene algebra with commutativity conditions is undecidable
por: de Amorim, Arthur Azevedo, et al.
Publicado: (2024)

A bargain for mergesorts -- How to prove your mergesort correct and stable, almost for free
por: Cohen, Cyril, et al.
Publicado: (2024)

Reasoning about concurrent loops and recursion with rely-guarantee rules
por: Hayes, Ian J., et al.
Publicado: (2025)

Drawing with Distance
por: Jacobs, Bart
Publicado: (2024)

A Probabilistic Choreography Language for PRISM
por: Carbone, Marco, et al.
Publicado: (2025)

A Lazy, Concurrent Convertibility Checker
por: Courant, Nathanaëlle, et al.
Publicado: (2025)

A feasible and unitary quantum programming language
por: Díaz-Caro, Alejandro, et al.
Publicado: (2023)

A Nominal Approach to Probabilistic Separation Logic
por: Li, John M., et al.
Publicado: (2024)

A Program Logic for Abstract (Hyper)Properties
por: Baldan, Paolo, et al.
Publicado: (2026)

A Demonic Outcome Logic for Randomized Nondeterminism
por: Zilberstein, Noam, et al.
Publicado: (2024)

A formalization of System I with type Top in Agda
por: Séttimo, Agustín, et al.
Publicado: (2026)

A programming language characterizing quantum polynomial time
por: Hainry, Emmanuel, et al.
Publicado: (2022)

PolyQEnt: A Polynomial Quantified Entailment Solver
por: Chatterjee, Krishnendu, et al.
Publicado: (2024)

A Formal Semantics of the GraalVM Intermediate Representation
por: Webb, Brae J., et al.
Publicado: (2021)

A Coq Library of Sets for Teaching Denotational Semantics
por: Cao, Qinxiang, et al.
Publicado: (2024)

A Formally Verified Procedure for Width Inference in FIRRTL
por: Wang, Keyin, et al.
Publicado: (2026)

A beginner guide to Iris, Coq and separation logic
por: Dietrich, Elizabeth
Publicado: (2021)

A uniform characterisation of the (a)synchronous must-preorder
por: Bernardi, Giovanni, et al.
Publicado: (2026)

A denotationally-based program logic for higher-order store
por: Aagaard, Frederik Lerbjerg, et al.
Publicado: (2023)

A Graded Modal Dependent Type Theory with Erasure, Formalized
por: Abel, Andreas, et al.
Publicado: (2026)

DateSAT: A Framework for Solving Date and Period Constraints
por: Cui, Leyi, et al.
Publicado: (2026)

A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
por: Chen, Zhibo, et al.
Publicado: (2023)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
por: Tsukada, Takeshi, et al.
Publicado: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
por: Coglio, Alessandro, et al.
Publicado: (2025)

A Program Logic for Under-approximating Worst-case Resource Usage
por: Jin, Ziyue, et al.
Publicado: (2025)

A Type System for Data Flow and Alias Analysis in ReScript
por: Lund, Nicky Ask, et al.
Publicado: (2024)

A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)
por: Vollmer, Victoria, et al.
Publicado: (2024)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
por: Kaye, George
Publicado: (2025)

Impredicativity in Linear Dependent Type Theory
por: Speight, Sam, et al.
Publicado: (2026)

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
por: Kappé, Tobias, et al.
Publicado: (2023)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
por: Ukhanov, Evgeny
Publicado: (2025)

Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency
por: Sulzmann, Martin
Publicado: (2026)

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
por: Tang, Xichen
Publicado: (2025)

Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
por: Zilberstein, Noam
Publicado: (2024)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
por: Grandury, Marcos, et al.
Publicado: (2025)

DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
por: Hu, Jason Z. S., et al.
Publicado: (2024)