Cover Image

Higher order differential calculus in mathlib

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Gouëzel, Sébastien
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Interpolation for the two-way modal mu-calculus
by: Kloibhofer, Johannes, et al.
Published: (2025)

Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
by: Hulak, David B., et al.
Published: (2026)

Cut-elimination for the alternation-free modal mu-calculus
by: Afshari, Bahareh, et al.
Published: (2025)

A concrete model for a typed linear algebraic lambda calculus
by: Díaz-Caro, Alejandro, et al.
Published: (2018)

The Constructive $μ$-calculus: Game Semantics and Non-Wellfounded Proof Systems
by: Pacheco, Leonardo
Published: (2026)

The calculus of neo-Peircean relations
by: Bonchi, Filippo, et al.
Published: (2025)

Resource approximation for the $λμ$-calculus
by: Barbarossa, Davide
Published: (2024)

The higher dimensional propositional calculus
by: Bucciarelli, Antonio, et al.
Published: (2022)

An implicit function theorem for the stream calculus
by: Boreale, Michele, et al.
Published: (2023)

A linear linear lambda-calculus
by: Díaz-Caro, Alejandro, et al.
Published: (2022)

Approximation theory for distant Bang calculus
by: Chardonnet, Kostia, et al.
Published: (2026)

On the complexity of normalization for the planar $λ$-calculus
by: Das, Anupam, et al.
Published: (2024)

Mechanized Undecidability of Higher-order beta-Matching (Extended Version)
by: Dudenhefner, Andrej
Published: (2026)

On the cut-elimination of the modal $μ$-calculus: Linear Logic to the rescue
by: Bauer, Esaïe, et al.
Published: (2025)

Formula size game and model checking for modal substitution calculus
by: Ahvonen, Veeti, et al.
Published: (2025)

The decohered ZX-calculus
by: Carette, Titouan, et al.
Published: (2025)

Higher-order Kripke models for intuitionistic and non-classical modal logics
by: Barroso-Nascimento, Victor
Published: (2025)

Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo
by: Komel, Anja Petković, et al.
Published: (2025)

Stability Property for the Call-by-Value $λ$-calculus through Taylor Expansion
by: Barbarossa, Davide
Published: (2024)

Higher-order bialgebraic semantics
by: Goncharov, Sergey, et al.
Published: (2024)

Encoding call-by-push-value in the pi-calculus
by: Bennetzen, Benjamin, et al.
Published: (2025)

A dependently-typed calculus of event telicity and culminativity
by: Kovalev, Pavel, et al.
Published: (2025)

A simple proof of the coincidence of observational and labeled equivalence of processes in applied pi-calculus
by: Mironov, Andrew M.
Published: (2025)

Wiring the Pi-calculus to Denotational Semantics
by: Sakayori, Ken, et al.
Published: (2026)

Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability
by: Bacci, Giorgio, et al.
Published: (2025)

Proof-theoretic Semantics for Second-order Logic
by: Gheorghiu, Alexander V., et al.
Published: (2025)

Countability constraints in order-theoretic approaches to computability
by: Hack, Pedro, et al.
Published: (2022)

Proof-theoretic Semantics for First-order Logic
by: Gheorghiu, Alexander V.
Published: (2024)

Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
by: Nogueira, Pablo, et al.
Published: (2022)

On semantics of first-order justification logic with binding modalities
by: Yavorskaya, Tatiana, et al.
Published: (2025)

Hypergraph rewriting and Causal structure of $λ-$calculus
by: Bajaj, Utkarsh
Published: (2024)

First-order Logic with Being a Thesis Modal Operator
by: Łyczak, Marcin
Published: (2024)

The proof theory and semantics of second-order (intuitionistic) tense logic
by: Becker, Justus, et al.
Published: (2026)

Higher-order circuits
by: Wilson, Matt
Published: (2026)

A linear proof language for second-order intuitionistic linear logic
by: Díaz-Caro, Alejandro, et al.
Published: (2023)

On the expressive power of inquisitive team logic and inquisitive first-order logic
by: Kontinen, Juha, et al.
Published: (2026)

The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
by: Oda, Yukihiro, et al.
Published: (2021)

Decomposing graphs into stable and ordered parts
by: Buffière, Hector, et al.
Published: (2025)

Impredicative Encodings of (Higher) Inductive Types
by: Awodey, Steve, et al.
Published: (2018)

S4 modal sequent calculus as intermediate logic and intermediate language
by: Caspar, Jean, et al.
Published: (2026)