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

From MaRDI portal
Changed an Item
Import241208061232 (talk | contribs)
Normalize DOI.
 
(12 intermediate revisions by 4 users not shown)
Property / DOI
 
Property / DOI: 10.1007/s10990-008-9038-0 / rank
Normal rank
 
Property / describes a project that uses
 
Property / describes a project that uses: ML / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: IMPS / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Depth First Search / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Regexp / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: ACL2 / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: HOL / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: ACL2s / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Cayenne / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Archive Formal Proofs / rank
 
Normal rank
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / full work available at URL
 
Property / full work available at URL: https://doi.org/10.1007/s10990-008-9038-0 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W2092268590 / rank
 
Normal rank
Property / cites work
 
Property / cites work: A predicative analysis of structural recursion / rank
 
Normal rank
Property / cites work
 
Property / cites work: Cayenne—a language with dependent types / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4736387 / rank
 
Normal rank
Property / cites work
 
Property / cites work: From regular expressions to deterministic automata / rank
 
Normal rank
Property / cites work
 
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. / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3894958 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Derivatives of Regular Expressions / rank
 
Normal rank
Property / cites work
 
Property / cites work: A formulation of the simple theory of types / rank
 
Normal rank
Property / cites work
 
Property / cites work: IMPS: An interactive mathematical proof system / rank
 
Normal rank
Property / cites work
 
Property / cites work: Verification of non-functional programs using interpretations in type theory / rank
 
Normal rank
Property / cites work
 
Property / cites work: Automata, Languages and Programming / rank
 
Normal rank
Property / cites work
 
Property / cites work: The under-appreciated unfold / rank
 
Normal rank
Property / cites work
 
Property / cites work: Termination of nested and mutually recursive algorithms / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4219036 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5287513 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proof producing synthesis of arithmetic and cryptographic hardware / rank
 
Normal rank
Property / cites work
 
Property / cites work: Efficient execution in an automated reasoning environment / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proof-directed debugging / rank
 
Normal rank
Property / cites work
 
Property / cites work: Regular expression pattern matching for XML / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proving and applying program transformations expressed with second-order patterns / rank
 
Normal rank
Property / cites work
 
Property / cites work: Building reliable, high-performance networks with the Nuprl proof development system / rank
 
Normal rank
Property / cites work
 
Property / cites work: The size-change principle for program termination / rank
 
Normal rank
Property / cites work
 
Property / cites work: Implicit parameters / rank
 
Normal rank
Property / cites work
 
Property / cites work: Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Termination Analysis with Calling Context Graphs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4945204 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Enumerating the strings of regular languages / rank
 
Normal rank
Property / cites work
 
Property / cites work: Partial functions in ACL2 / rank
 
Normal rank
Property / cites work
 
Property / cites work: HOLCF = HOL + LCF / rank
 
Normal rank
Property / cites work
 
Property / cites work: Isabelle/HOL. A proof assistant for higher-order logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: A Thread of HOL Development / rank
 
Normal rank
Property / cites work
 
Property / cites work: On equivalents of well-foundedness. An experiment in MIZAR / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4365106 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2723408 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Applications of Polytypism in Theorem Proving / rank
 
Normal rank
Property / cites work
 
Property / cites work: Programming Techniques: Regular expression search algorithm / rank
 
Normal rank
Property / cites work
 
Property / cites work: Dependent types for program termination verification / rank
 
Normal rank
Property / DOI
 
Property / DOI: 10.1007/S10990-008-9038-0 / rank
 
Normal rank

Latest revision as of 13:47, 10 December 2024

scientific article
Language Label Description Also known as
English
Adapting functional programs to higher order logic
scientific article

    Statements

    Adapting functional programs to higher order logic (English)
    0 references
    0 references
    0 references
    13 July 2009
    0 references
    higher-order logic
    0 references
    recursive definition
    0 references
    termination
    0 references
    well-foundedness
    0 references
    regular expression pattern matching
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers