scientific article; zbMATH DE number 7204440
From MaRDI portal
Publication:5111317
Recommendations
Cites work
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 3485174 (Why is no real title available?)
- scientific article; zbMATH DE number 3400430 (Why is no real title available?)
- A Declarative Language for the Coq Proof Assistant
- A framework for defining logics
- A two-level logic approach to reasoning about computations
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
- Abella: a system for reasoning about relational specifications
- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
- Contextual modal type theory
- Engineering formal metatheory
- Explicit substitutions
- Higher-order superposition for dependent types
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Inductive beluga: programming proofs
- Introduction to generalized type systems
- Practical foundations for programming languages
- Programming inductive proofs. A new approach based on contextual types
- Reasoning with higher-order abstract syntax and contexts: a comparison
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Theorem Proving in Higher Order Logics
Cited in
(7)- Mechanized metatheory revisited
- Mechanizing metatheory without typing contexts
- Mechanizing type environments in weak HOAS
- Theorem Proving in Higher Order Logics
- System F in Agda, for fun and profit
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
- A weak HOAS approach to the POPLmark challenge
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)
