Mechanizing type environments in weak HOAS
From MaRDI portal
Publication:897934
DOI10.1016/J.TCS.2015.07.019zbMATH Open1332.68202OpenAlexW892879558MaRDI QIDQ897934FDOQ897934
Alberto Ciaffaglione, Ivan Scagnetto
Publication date: 8 December 2015
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2015.07.019
Recommendations
Cites Work
- Title not available (Why is that?)
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Theorem Proving in Higher Order Logics
- Nominal logic, a first order theory of names and binding
- A framework for defining logics
- A new approach to abstract syntax with variable binding
- Types and programing languages
- Engineering formal metatheory
- \(\pi\)-calculus in (Co)inductive-type theory
- Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
- Title not available (Why is that?)
- Title not available (Why is that?)
- Parametric higher-order abstract syntax for mechanized semantics
- Consistency of the theory of contexts
- Using typed lambda calculus to implement formal systems on a machine
- Title not available (Why is that?)
- Imperative object-based calculi in co-inductive type theories
- The theory of contexts for first order and higher order abstract syntax
- Title not available (Why is that?)
- A natural deduction approach to dynamic logic
- Title not available (Why is that?)
- Boxes go bananas
Cited In (2)
Uses Software
This page was built for publication: Mechanizing type environments in weak HOAS
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q897934)
