Alternating parity Krivine automata

DOI10.1007/978-3-662-44522-8_10MaRDI QIDQ2922007zbMATH OpenOpenAlexFDO

Authors Florian Bruse

Publication date 14 October 2014

Published in Mathematical Foundations of Computer Science 2014 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-44522-8_10

zbMATH Keywords

\(\lambda \)-calculusfixpoint logichigher-order modal fixpoint logicKrivine machine

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Modal logic (including the logic of norms) (03B45) Automata and formal grammars in connection with logical questions (03D05) Formal languages and automata (68Q45)

Recommendations

• Alternation is strict for higher-order modal fixpoint logic
• CONCUR 2004 - Concurrency Theory
• The Complexity of Model Checking Higher-Order Fixpoint Logic
• Space-efficient fragments of higher-order fixpoint logic
• The complexity of model-checking tail-recursive higher-order fixpoint logic

Cited in

(5)

• Krivine machines and higher-order schemes
• A type-directed negation elimination
• Alternation is strict for higher-order modal fixpoint logic
• CONCUR 2004 - Concurrency Theory
• A cyclic proof system for HFL\(_\mathbb{N}\)

This page was built for publication: Alternating parity Krivine automata

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