Copertina

Redex -> Coq: towards a theory of decidability of Redex's reduction semantics

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Soldevila, Mallku, Ribeiro, Rodrigo, Ziliani, Beta
Natura:	Preprint
Pubblicazione:	2024
Soggetti:	Logic in Computer Science Programming Languages
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

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

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

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

Higher-order bialgebraic semantics
di: Goncharov, Sergey, et al.
Pubblicazione: (2024)

A Graphical Interface for Category Theory Proofs in Coq
di: Chabassier, Luc
Pubblicazione: (2025)

Compositional theories for host-core languages
di: Trotta, Davide, et al.
Pubblicazione: (2020)

Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
di: Ye, Kangfeng, et al.
Pubblicazione: (2023)

Syntactically and semantically regular languages of lambda-terms coincide through logical relations
di: Moreau, Vincent, et al.
Pubblicazione: (2023)

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

GPU accelerated program synthesis: Enumerate semantics, not syntax!
di: Berger, Martin, et al.
Pubblicazione: (2025)

Teaching Divisibility and Binomials with Coq
di: Boldo, Sylvie, et al.
Pubblicazione: (2024)

Meaningfulness and Genericity in a Subsuming Framework
di: Kesner, Delia, et al.
Pubblicazione: (2024)

Towards a Higher-Order Bialgebraic Denotational Semantics
di: Goncharov, Sergey, et al.
Pubblicazione: (2026)

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

JAX Autodiff from a Linear Logic Perspective (Extended Version)
di: Giusti, Giulia, et al.
Pubblicazione: (2025)

Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir
di: Castagna, Giuseppe, et al.
Pubblicazione: (2024)

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

Linear effects, exceptions, and resource safety: a Curry-Howard correspondence for destructors
di: Congard, Sidney, et al.
Pubblicazione: (2025)

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
di: Elad, Neta, et al.
Pubblicazione: (2023)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
di: Verscht, Lena, et al.
Pubblicazione: (2024)

Operational methods in semantics
di: Amadio, Roberto M.
Pubblicazione: (2025)

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

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

Structural Temporal Logic for Mechanized Program Verification
di: Ioannidis, Eleftherios, et al.
Pubblicazione: (2024)

An Introduction to Different Approaches to Initial Semantics
di: Lamiaux, Thomas, et al.
Pubblicazione: (2024)

More Church-Rosser Proofs in BELUGA
di: Momigliano, Alberto, et al.
Pubblicazione: (2024)

Bialgebraic Reasoning on Higher-Order Program Equivalence
di: Goncharov, Sergey, et al.
Pubblicazione: (2024)

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

Syntax-Guided Automated Program Repair for Hyperproperties
di: Beutner, Raven, et al.
Pubblicazione: (2024)

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

Hybrid Intersection Types for PCF (Extended Version)
di: Barenbaum, Pablo, et al.
Pubblicazione: (2024)

Verifying Lock-free Search Structure Templates
di: Patel, Nisarg, et al.
Pubblicazione: (2024)

Functional Array Programming in an Extended Pi-Calculus
di: Hüttel, Hans, et al.
Pubblicazione: (2024)

An Abstract Domain for Heap Commutativity (Extended Version)
di: Pincus, Jared, et al.
Pubblicazione: (2024)

Verifying Functional Correctness Properties At the Level of Java Bytecode
di: Paganoni, Marco, et al.
Pubblicazione: (2024)

Polymorphic Metaprogramming with Memory Management -- An Adjoint Analysis of Metaprogramming
di: Jang, Junyoung, et al.
Pubblicazione: (2024)

The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective)
di: Accattoli, Beniamino
Pubblicazione: (2024)

Useful Evaluation: Syntax and Semantics (Technical Report)
di: Barenbaum, Pablo, et al.
Pubblicazione: (2024)

Linear Contextual Metaprogramming and Session Types
di: Ângelo, Pedro, et al.
Pubblicazione: (2024)

Domain Reasoning in TopKAT
di: Zhang, Cheng, et al.
Pubblicazione: (2024)