Adapting functional programs to higher order logic (Q1029815): Difference between revisions

@@ Property / DOI @@
-.1007/s10990-008-9038-0
@@ Property / DOI: 10.1007/s10990-008-9038-0 / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+ACL2s
@@ Property / describes a project that uses: ACL2s / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Cayenne
@@ Property / describes a project that uses: Cayenne / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / 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/s10990-008-9038-0
+Normal rank
@@ Property / OpenAlex ID @@
+W2092268590
@@ Property / OpenAlex ID: W2092268590 / rank @@
+Normal rank
@@ Property / cites work @@
+A predicative analysis of structural recursion
@@ Property / cites work: A predicative analysis of structural recursion / rank @@
+Normal rank
@@ Property / cites work @@
+Cayenne—a language with dependent types
@@ Property / cites work: Cayenne—a language with dependent types / rank @@
+Normal rank
@@ Property / cites work @@
+Q4736387
@@ Property / cites work: Q4736387 / rank @@
+Normal rank
@@ Property / cites work @@
+From regular expressions to deterministic automata
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Q3894958
@@ Property / cites work: Q3894958 / rank @@
+Normal rank
@@ Property / cites work @@
+Derivatives of Regular Expressions
@@ Property / cites work: Derivatives of Regular Expressions / rank @@
+Normal rank
@@ Property / cites work @@
+A formulation of the simple theory of types
@@ Property / cites work: A formulation of the simple theory of types / rank @@
+Normal rank
@@ Property / cites work @@
+IMPS: An interactive mathematical proof system
@@ Property / cites work: IMPS: An interactive mathematical proof system / rank @@
+Normal rank
@@ Property / cites work @@
+Verification of non-functional programs using interpretations in type theory
+Normal rank
@@ Property / cites work @@
+Automata, Languages and Programming
@@ Property / cites work: Automata, Languages and Programming / rank @@
+Normal rank
@@ Property / cites work @@
+The under-appreciated unfold
@@ Property / cites work: The under-appreciated unfold / rank @@
+Normal rank
@@ Property / cites work @@
+Termination of nested and mutually recursive algorithms
+Normal rank
@@ Property / cites work @@
+Q4219036
@@ Property / cites work: Q4219036 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+Proof producing synthesis of arithmetic and cryptographic hardware
+Normal rank
@@ Property / cites work @@
+Efficient execution in an automated reasoning environment
+Normal rank
@@ Property / cites work @@
+Proof-directed debugging
@@ Property / cites work: Proof-directed debugging / rank @@
+Normal rank
@@ Property / cites work @@
+Regular expression pattern matching for XML
@@ Property / cites work: Regular expression pattern matching for XML / rank @@
+Normal rank
@@ Property / cites work @@
+Proving and applying program transformations expressed with second-order patterns
+Normal rank
@@ Property / cites work @@
+Building reliable, high-performance networks with the Nuprl proof development system
+Normal rank
@@ Property / cites work @@
+The size-change principle for program termination
@@ Property / cites work: The size-change principle for program termination / rank @@
+Normal rank
@@ Property / cites work @@
+Implicit parameters
@@ Property / cites work: Implicit parameters / rank @@
+Normal rank
@@ Property / cites work @@
+Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
+Normal rank
@@ Property / cites work @@
+Termination Analysis with Calling Context Graphs
@@ Property / cites work: Termination Analysis with Calling Context Graphs / rank @@
+Normal rank
@@ Property / cites work @@
+Q4945204
@@ Property / cites work: Q4945204 / rank @@
+Normal rank
@@ Property / cites work @@
+Enumerating the strings of regular languages
@@ Property / cites work: Enumerating the strings of regular languages / rank @@
+Normal rank
@@ Property / cites work @@
+Partial functions in ACL2
@@ Property / cites work: Partial functions in ACL2 / rank @@
+Normal rank
@@ Property / cites work @@
+HOLCF = HOL + LCF
@@ Property / cites work: HOLCF = HOL + LCF / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+A Thread of HOL Development
@@ Property / cites work: A Thread of HOL Development / rank @@
+Normal rank
@@ Property / cites work @@
+On equivalents of well-foundedness. An experiment in MIZAR
+Normal rank
@@ Property / cites work @@
+Q4365106
@@ Property / cites work: Q4365106 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2723408
@@ Property / cites work: Q2723408 / rank @@
+Normal rank
@@ Property / cites work @@
+Applications of Polytypism in Theorem Proving
@@ Property / cites work: Applications of Polytypism in Theorem Proving / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Techniques: Regular expression search algorithm
+Normal rank
@@ Property / cites work @@
+Dependent types for program termination verification
+Normal rank
@@ Property / DOI @@
+.1007/S10990-008-9038-0
@@ Property / DOI: 10.1007/S10990-008-9038-0 / rank @@
+Normal rank