Structural analysis of narratives with the Coq proof assistant
DOI10.1007/978-3-642-22863-6_7zbMATH Open1342.68280DBLPconf/itp/BosserCFC11OpenAlexW4300749781WikidataQ57516617 ScholiaQ57516617MaRDI QIDQ3087995FDOQ3087995
Authors: Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza 
Publication date: 17 August 2011
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://research.tees.ac.uk/en/publications/813c661d-f423-4ed8-ad31-b53da2d22919
Recommendations
- Linear Logic for non-linear storytelling
- Proof assistants for natural language semantics
- Narrative Structure of Mathematical Texts
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Interactive proofs in higher-order concurrent separation logic
Logic in artificial intelligence (68T27) Proof-theoretic aspects of linear logic and other substructural logics (03F52)
Cites Work
- Linear logic
- Title not available (Why is that?)
- Generating plans in linear logic. I: Actions as proofs
- Generating plans in linear logic. II: A geometry of conjunctive actions
- Title not available (Why is that?)
- Narratives in the Situation Calculus
- A simple declarative language for describing narratives with actions
- Plans, actions and dialogues using linear logic
- Linear Logic for non-linear storytelling
Cited In (20)
- A formal semantics of nested atomic sections with thread escape
- Verifying relative safety, accuracy, and termination for program approximations
- A realizability interpretation of Church's simple theory of types
- Formalizing Soundness of Contextual Effects
- Proofs, programs, processes
- Explaining Gabriel-Zisman localization to the computer
- Some aspects of narrative method
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- An effective proof of the well-foundedness of the multiset path ordering
- Targeted configuration of an SMT solver
- Experimenting Formal Proofs of Petri Nets Refinements
- Linear Logic for non-linear storytelling
- Automated verification of the parallel Bellman-Ford algorithm
- Regular language representations in the constructive type theory of Coq
- Local Termination
- Proof assistants: history, ideas and future
- TPS: A hybrid automatic-interactive system for developing proofs
- Executing and verifying higher-order functional-imperative programs in Maude
- An introduction to univalent foundations for mathematicians
- Lem: a lightweight tool for heavyweight semantics
Uses Software
This page was built for publication: Structural analysis of narratives with the Coq proof assistant
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3087995)
