Image de couverture de livre

Small Scale Reflection for the Working Lean User

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Gladshtein, Vladimir, Pîrlea, George, Sergey, Ilya
Format:	Preprint
Publié:	2024
Sujets:	Programming Languages Logic in Computer Science
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Mechanised Hypersafety Proofs about Structured Data: Extended Version
par: Gladshtein, Vladimir, et autres
Publié: (2024)

Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference
par: Yang, Ziyi, et autres
Publié: (2026)

CSLib: The Lean Computer Science Library
par: Barrett, Clark, et autres
Publié: (2026)

Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
par: Montesi, Fabrizio, et autres
Publié: (2026)

Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)
par: Henson, Christopher, et autres
Publié: (2026)

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

Semantically Reflected Programs
par: Kamburjan, Eduard, et autres
Publié: (2025)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
par: Kaye, George
Publié: (2025)

Abstract Operational Methods for Call-by-Push-Value
par: Goncharov, Sergey, et autres
Publié: (2024)

Bialgebraic Reasoning on Higher-Order Program Equivalence
par: Goncharov, Sergey, et autres
Publié: (2024)

Logical Predicates in Higher-Order Mathematical Operational Semantics
par: Goncharov, Sergey, et autres
Publié: (2024)

Higher-order bialgebraic semantics
par: Goncharov, Sergey, et autres
Publié: (2024)

Bialgebraic Reasoning on Stateful Languages
par: Goncharov, Sergey, et autres
Publié: (2025)

Towards a Higher-Order Bialgebraic Denotational Semantics
par: Goncharov, Sergey, et autres
Publié: (2026)

Certified Program Synthesis with a Multi-Modal Verifier
par: Feng, Yueyang, et autres
Publié: (2026)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
par: Li, Jinzheng, et autres
Publié: (2026)

Kleene algebra with commutativity conditions is undecidable
par: de Amorim, Arthur Azevedo, et autres
Publié: (2024)

Proceedings 9th edition of Working Formal Methods Symposium
par: Arusoaie, Andrei, et autres
Publié: (2025)

Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages
par: Carette, TItouan, et autres
Publié: (2022)

Making first order linear logic a generating grammar
par: Slavnov, Sergey
Publié: (2022)

The Hidden Strength of Costrong Functors
par: Balan, Adriana, et autres
Publié: (2025)

A programming language combining quantum and classical control
par: Dave, Kinnari, et autres
Publié: (2025)

Towards a Higher-Order Mathematical Operational Semantics
par: Goncharov, Sergey, et autres
Publié: (2022)

A Complete Theory of Sequential Digital Circuits: Denotational, Operational and Algebraic Semantics
par: Ghica, Dan R., et autres
Publié: (2022)

Impredicativity in Linear Dependent Type Theory
par: Speight, Sam, et autres
Publié: (2026)

Structural Temporal Logic for Mechanized Program Verification
par: Ioannidis, Eleftherios, et autres
Publié: (2024)

An Introduction to Different Approaches to Initial Semantics
par: Lamiaux, Thomas, et autres
Publié: (2024)

More Church-Rosser Proofs in BELUGA
par: Momigliano, Alberto, et autres
Publié: (2024)

A Nominal Approach to Probabilistic Separation Logic
par: Li, John M., et autres
Publié: (2024)

Syntax-Guided Automated Program Repair for Hyperproperties
par: Beutner, Raven, et autres
Publié: (2024)

DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
par: Hu, Jason Z. S., et autres
Publié: (2024)

Hybrid Intersection Types for PCF (Extended Version)
par: Barenbaum, Pablo, et autres
Publié: (2024)

Verifying Lock-free Search Structure Templates
par: Patel, Nisarg, et autres
Publié: (2024)

Functional Array Programming in an Extended Pi-Calculus
par: Hüttel, Hans, et autres
Publié: (2024)

An Abstract Domain for Heap Commutativity (Extended Version)
par: Pincus, Jared, et autres
Publié: (2024)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
par: Verscht, Lena, et autres
Publié: (2024)

Verifying Functional Correctness Properties At the Level of Java Bytecode
par: Paganoni, Marco, et autres
Publié: (2024)

Polymorphic Metaprogramming with Memory Management -- An Adjoint Analysis of Metaprogramming
par: Jang, Junyoung, et autres
Publié: (2024)

The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective)
par: Accattoli, Beniamino
Publié: (2024)

Useful Evaluation: Syntax and Semantics (Technical Report)
par: Barenbaum, Pablo, et autres
Publié: (2024)