Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569): Difference between revisions

@@ Property / author @@
-Amy P. Felty
@@ Property / author: Amy P. Felty / rank @@
-Normal rank
@@ Property / author @@
+Amy P. Felty
@@ Property / author: Amy P. Felty / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+T15
@@ Property / Mathematics Subject Classification ID: 68T15 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+B70
@@ Property / Mathematics Subject Classification ID: 03B70 / rank @@
+Normal rank
@@ Property / zbMATH DE Number @@
+6062061
@@ Property / zbMATH DE Number: 6062061 / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+logical frameworks
@@ Property / zbMATH Keywords: logical frameworks / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+higher-order abstract syntax
@@ Property / zbMATH Keywords: higher-order abstract syntax / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+interactive theorem proving
@@ Property / zbMATH Keywords: interactive theorem proving / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+induction
@@ Property / zbMATH Keywords: induction / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+variable binding
@@ Property / zbMATH Keywords: variable binding / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+Isabelle/HOL
@@ Property / zbMATH Keywords: Isabelle/HOL / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+Coq
@@ Property / zbMATH Keywords: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HYBRID
@@ Property / describes a project that uses: HYBRID / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Ott
@@ Property / describes a project that uses: Ott / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PVS
@@ Property / describes a project that uses: PVS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Abella
@@ Property / describes a project that uses: Abella / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LEGO
@@ Property / describes a project that uses: LEGO / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PoplMark
@@ Property / describes a project that uses: PoplMark / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nominal Isabelle
@@ Property / describes a project that uses: Nominal Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Bedwyr
@@ Property / describes a project that uses: Bedwyr / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+mini-ML
@@ Property / describes a project that uses: mini-ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Lolli
@@ Property / describes a project that uses: Lolli / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isar
@@ Property / describes a project that uses: Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/ZF
@@ Property / describes a project that uses: Isabelle/ZF / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Twelf
@@ Property / describes a project that uses: Twelf / 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.1007/s10817-010-9194-x
+Normal rank
@@ Property / OpenAlex ID @@
+W2140849218
@@ Property / OpenAlex ID: W2140849218 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:438569