Typing Weak MSOL Properties
From MaRDI portal
Publication:2949449
DOI10.1007/978-3-662-46678-0_22zbMath1448.68315arXiv1609.02753OpenAlexW310657667MaRDI QIDQ2949449
Sylvain Salvati, Igor Walukiewicz
Publication date: 1 October 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1609.02753
denotational semanticsrecognizabilityhigher-order model checkingfinite state methodssimply typed \(\lambda\)Y-calculusweak monadic second order logic
Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Higher-order logic (03B16)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Fixed-point operations on ccc's. I
- Domain theory in logical form
- An algebraic proof of Rabin's tree theorem
- Exact Flow Analysis by Higher-Order Model Checking
- Saturation-Based Model Checking of Higher-Order Recursion Schemes.
- Evaluation is MSOL compatible
- Krivine Machines and Higher-Order Schemes
- Loader and Urzyczyn Are Logically Related
- A filter lambda model and the completeness of type assignment
- Completeness, invariance and λ-definability
- Functional reactive types
- Compositional higher-order model checking via ω -regular games over Böhm trees
- C-SHORe
- Higher-order multi-parameter tree transducers and recursion schemes for program verification
- Types and higher-order recursion schemes for verification of higher-order programs
- Using Models to Model-Check Recursive Schemes
- Programming Languages and Systems
- Collapsible Pushdown Automata and Recursion Schemes
- Model Checking Higher-Order Programs
- A type-directed abstraction refinement approach to higher-order model checking
- Verifying higher-order functional programs with pattern-matching algebraic data types
- A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus
- Finitary PCF is not decidable
