scientific article; zbMATH DE number 7204440

DOI10.4230/LIPICS.FSCD.2017.21zbMATH Open1434.03030MaRDI QIDQ5111317FDOQ5111317

Authors: Brigitte Pientka, Gert Smolka, Jonas Pilgaard Kaiser 

Publication date: 26 May 2020

Title of this publication is not available (Why is that?)

Recommendations

• A weak HOAS approach to the POPLmark challenge
• Theorem Proving in Higher Order Logics
• A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
• Reasoning with higher-order abstract syntax and contexts: a comparison
• Mechanizing proofs with logical relations -- Kripke-style

zbMATH Keywords

higher-order abstract syntaxSystem Fpure type systemscontextual reasoningde Bruijn syntax

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Type theory (03B38)

Cites Work

• Abella: A System for Reasoning about Relational Specifications
• Theorem Proving in Higher Order Logics
• Title not available (Why is that?)
• A framework for defining logics
• Contextual modal type theory
• A two-level logic approach to reasoning about computations
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Programming inductive proofs. A new approach based on contextual types
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• A Declarative Language for the Coq Proof Assistant
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Title not available (Why is that?)
• Reasoning with higher-order abstract syntax and contexts: a comparison
• Practical foundations for programming languages
• Title not available (Why is that?)
• Engineering formal metatheory
• Explicit substitutions
• Introduction to generalized type systems
• Higher-order superposition for dependent types
• Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
• Inductive Beluga: Programming Proofs

Cited In (3)

• Mechanized metatheory revisited
• Theorem Proving in Higher Order Logics
• A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL

Uses Software

• Coq
• HYBRID
• Beluga
• Twelf
• Automath
• Abella
• PoplMark

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111317)