scientific article; zbMATH DE number 7204440

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

Jonas Pilgaard Kaiser, Brigitte Pientka, Gert Smolka

Publication date: 26 May 2020

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

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

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Abella: A System for Reasoning about Relational Specifications
• Theorem Proving in Higher Order Logics
• 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 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
• Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison
• Practical foundations for programming languages
• 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 (1)

• Mechanized metatheory revisited

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)