Model-checking games for typed -calculi

DOI10.1016/J.ENTCS.2007.02.021MaRDI QIDQ2864164zbMATH OpenOpenAlexFDO

Authors Colin Stirling

Publication date 6 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2007.02.021

zbMATH Keywords

gamestyped lambda calculushigher-order schemeshigher-order matching

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• Model checking games for the quantitative \(\mu \)-calculus
• Model checking games for the quantitative \(\mu\)-calculus
• scientific article; zbMATH DE number 1223630
• Games and model checking for guarded logics
• Game-based local model checking for the coalgebraic \(\mu\)-calculus
• Innocent game models of untyped -calculus
• scientific article; zbMATH DE number 1342276
• Game-theoretic semantics for \(\mathrm{ATL}^+\) with applications to model checking
• Game semantics and uniqueness of type inhabitance in the simply-typed -calculus

Cites work

• scientific article; zbMATH DE number 1223619 (Why is no real title available?)
• scientific article; zbMATH DE number 2061708 (Why is no real title available?)
• scientific article; zbMATH DE number 1929935 (Why is no real title available?)
• scientific article; zbMATH DE number 2086674 (Why is no real title available?)
• scientific article; zbMATH DE number 2087432 (Why is no real title available?)
• A Game-Theoretic Approach to Deciding Higher-Order Matching
• A representation of trees by languages. I
• An automata-theoretical characterization of the OI-hierarchy
• Computer Science Logic
• Decidability of DPDA equivalence
• Decidability of all minimal models
• Decidability of bisimulation equivalence for process generating context-free languages
• Decidability of fourth-order matching
• Foundations of Software Science and Computational Structures
• Higher Order   Matching is Undecidable
• Indexed Grammars—An Extension of Context-Free Grammars
• Nested Stack Automata
• The IO- and OI-hierarchies
• Third order matching is decidable
• \(L(A)=L(B)\)? A simplified decidability proof.
• \(L(A)=L(B)\)? decidability results from complete formal systems

Cited in

(3)

• scientific article; zbMATH DE number 1342276 (Why is no real title available?)
• scientific article; zbMATH DE number 1223630 (Why is no real title available?)
• Innocent game models of untyped -calculus

This page was built for publication: Model-checking games for typed \(\lambda\)-calculi

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2864164)