Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
From MaRDI portal
Publication:6492754
DOI10.1007/978-3-031-38499-8_20MaRDI QIDQ6492754
Publication date: 26 April 2024
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Unnamed Item
- Unnamed Item
- Orderings for term-rewriting systems
- Mechanizing and improving dependency pairs
- From Jinja bytecode to term rewriting: a complexity reflecting transformation
- On probabilistic term rewriting
- Termination of term rewriting using dependency pairs
- Inferring expected runtimes of probabilistic integer programs using expected sizes
- Automated termination analysis of polynomial probabilistic programs
- Computing expected runtimes for constant probability programs
- Analyzing innermost runtime complexity of term rewriting by dependency pairs
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Automating the dependency pair method
- Probabilistic Termination
- Probabilistic Termination by Monadic Affine Sized Typing
- Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
- Term Rewriting and All That
- A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog
- mu-term: Verify Termination Properties Automatically (System Description)
- Expected Runtime Analyis by Program Verification
- Termination Analysis of Probabilistic Programs with Martingales
- Nagoya Termination Tool
- Automated Termination Analysis of Java Bytecode by Term Rewriting
- Term Rewriting and Applications
- Logic for Programming, Artificial Intelligence, and Reasoning
- Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
This page was built for publication: Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs