scientific article; zbMATH DE number 7204440

DOI10.4230/LIPIcs.FSCD.2017.21zbMath1434.03030MaRDI QIDQ5111317

Brigitte Pientka, Gert Smolka, Jonas Pilgaard Kaiser

Publication date: 26 May 2020

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

pure type systemshigher-order abstract syntaxSystem Fcontextual reasoningde Bruijn syntax

Mathematics Subject Classification ID

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

Related Items

Mechanized metatheory revisited

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• A two-level logic approach to reasoning about computations
• Practical Foundations for Programming Languages
• Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
• Programming Inductive Proofs
• Engineering formal metatheory
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Inductive Beluga: Programming Proofs
• A Declarative Language for the Coq Proof Assistant
• A framework for defining logics
• Explicit substitutions
• Introduction to generalized type systems
• Higher-order superposition for dependent types
• Abella: A System for Reasoning about Relational Specifications
• Contextual modal type theory
• Theorem Proving in Higher Order Logics
• Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison