Mechanizing type environments in weak HOAS (Q897934): Difference between revisions

@@ Property / describes a project that uses @@
+PoplMark
@@ Property / describes a project that uses: PoplMark / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Beluga
@@ Property / describes a project that uses: Beluga / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.tcs.2015.07.019
+Normal rank
@@ Property / OpenAlex ID @@
+W892879558
@@ Property / OpenAlex ID: W892879558 / rank @@
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024831
@@ Property / cites work: Q3024831 / rank @@
+Normal rank
@@ Property / cites work @@
+Nominal logic, a first order theory of names and binding
+Normal rank
@@ Property / cites work @@
+Q4535076
@@ Property / cites work: Q4535076 / rank @@
+Normal rank
@@ Property / cites work @@
+Parametric higher-order abstract syntax for mechanized semantics
+Normal rank
@@ Property / cites work @@
+Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
+Normal rank
@@ Property / cites work @@
+\(\pi\)-calculus in (Co)inductive-type theory
@@ Property / cites work: \(\pi\)-calculus in (Co)inductive-type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Q4012880
@@ Property / cites work: Q4012880 / rank @@
+Normal rank
@@ Property / cites work @@
+A natural deduction approach to dynamic logic
@@ Property / cites work: A natural deduction approach to dynamic logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q3408131
@@ Property / cites work: Q3408131 / rank @@
+Normal rank
@@ Property / cites work @@
+Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
+Normal rank
@@ Property / cites work @@
+Consistency of the theory of contexts
@@ Property / cites work: Consistency of the theory of contexts / rank @@
+Normal rank
@@ Property / cites work @@
+Q4992397
@@ Property / cites work: Q4992397 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2778806
@@ Property / cites work: Q2778806 / rank @@
+Normal rank
@@ Property / cites work @@
+The Theory of Contexts for First Order and Higher Order Abstract Syntax
+Normal rank
@@ Property / cites work @@
+Q5417200
@@ Property / cites work: Q5417200 / rank @@
+Normal rank
@@ Property / cites work @@
+Using typed lambda calculus to implement formal systems on a machine
+Normal rank
@@ Property / cites work @@
+Engineering formal metatheory
@@ Property / cites work: Engineering formal metatheory / rank @@
+Normal rank
@@ Property / cites work @@
+A new approach to abstract syntax with variable binding
+Normal rank
@@ Property / cites work @@
+Boxes go bananas
@@ Property / cites work: Boxes go bananas / rank @@
+Normal rank
@@ Property / cites work @@
+Q2769442
@@ Property / cites work: Q2769442 / rank @@
+Normal rank