Mechanizing type environments in weak HOAS

DOI10.1016/J.TCS.2015.07.019MaRDI QIDQ897934zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• A weak HOAS approach to the POPLmark challenge
• Strongly typed term representations in Coq
• Parametric higher-order abstract syntax for mechanized semantics
• Mechanizing proofs with logical relations -- Kripke-style
• scientific article; zbMATH DE number 7204440

Cites work

• scientific article; zbMATH DE number 1701361 (Why is no real title available?)
• scientific article; zbMATH DE number 2185657 (Why is no real title available?)
• scientific article; zbMATH DE number 65532 (Why is no real title available?)
• scientific article; zbMATH DE number 1754648 (Why is no real title available?)
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• A framework for defining logics
• A natural deduction approach to dynamic logic
• A new approach to abstract syntax with variable binding
• A weak HOAS approach to the POPLmark challenge
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism
• Consistency of the theory of contexts
• Engineering formal metatheory
• Imperative object-based calculi in co-inductive type theories
• Nominal logic, a first order theory of names and binding
• Parametric higher-order abstract syntax for mechanized semantics
• 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
• Theorem Proving in Higher Order Logics
• Types and programing languages
• Using typed lambda calculus to implement formal systems on a machine
• \(\pi\)-calculus in (Co)inductive-type theory

Cited in

(4)

• Mechanizing metatheory without typing contexts
• \(\mathrm{HO}\pi\) in Coq
• A weak HOAS approach to the POPLmark challenge
• Strongly typed term representations in Coq

Describes a project that uses

Uses Software

• Coq
• Beluga
• PoplMark

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)