Mechanizing type environments in weak HOAS

DOI10.1016/j.tcs.2015.07.019zbMath1332.68202OpenAlexW892879558MaRDI QIDQ897934

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

zbMATH Keywords

type theorylogical frameworksHOASPOPLmark challenge

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (1)

\(\mathrm{HO}\pi\) in Coq

Uses Software

• Coq
• Beluga
• PoplMark

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Using typed lambda calculus to implement formal systems on a machine
• A new approach to abstract syntax with variable binding
• \(\pi\)-calculus in (Co)inductive-type theory
• Nominal logic, a first order theory of names and binding
• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
• The Theory of Contexts for First Order and Higher Order Abstract Syntax
• Engineering formal metatheory
• A framework for defining logics
• A natural deduction approach to dynamic logic
• Parametric higher-order abstract syntax for mechanized semantics
• Boxes go bananas
• Consistency of the theory of contexts
• Theorem Proving in Higher Order Logics
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)

This page was built for publication: Mechanizing type environments in weak HOAS