Plugging-in proof development environments usingLocksinLF
From MaRDI portal
Publication:4691186
DOI10.1017/S0960129518000105zbMath1400.68195MaRDI QIDQ4691186
Petar Maksimović, Ivan Scagnetto, Luigi Liquori, Furio Honsell
Publication date: 19 October 2018
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Light logics and optimal reduction: completeness and complexity
- Light linear logic
- Proof-functional connectives and realizability
- Propositional lax logic
- \(\pi\)-calculus in (Co)inductive-type theory
- Autarkic computations in formal proofs
- Proof-theoretic semantics, self-contradiction, and the format of deductive reasoning
- An open logical framework
- A Framework for Defining Logical Frameworks
- L ax F: Side Conditions and External Evidence as Monads
- Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)
- Contextual modal type theory
- Mechanizing metatheory in a logical framework
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
This page was built for publication: Plugging-in proof development environments usingLocksinLF
