Copertina

A formalization of System I with type Top in Agda

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Séttimo, Agustín, Sottile, Cristian, Manzino, Cecilia
Natura:	Preprint
Pubblicazione:	2026
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

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

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)

Multi types and reasonable space
di: Accattoli, Beniamino, et al.
Pubblicazione: (2022)

Simply typed convertibility is TOWER-complete even for safe lambda-terms
di: Nguyên, Lê Thành Dũng
Pubblicazione: (2023)

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

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

Orthologic Type Systems
di: Guilloud, Simon, et al.
Pubblicazione: (2025)

Strong normalization through idempotent intersection types: a new syntactical approach
di: Barenbaum, Pablo, et al.
Pubblicazione: (2025)

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

Multi-paradigm Logic Programming in the ${\cal E}$rgoAI System
di: Kifer, Michael, et al.
Pubblicazione: (2026)

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

Frex: dependently-typed algebraic simplification
di: Allais, Guillaume, et al.
Pubblicazione: (2023)

On Representability of Multiple-Valued Functions by Linear Lambda Terms Typed with Second-order Polymorphic Type System
di: Matsuoka, Satoshi
Pubblicazione: (2026)

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

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

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

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

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

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

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

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

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

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

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

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

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)

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

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

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

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

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

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

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

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

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

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

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

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

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