Partial and nested recursive function definitions in higher-order logic (Q972425): Difference between revisions

From MaRDI portal
Changed an Item
ReferenceBot (talk | contribs)
Changed an Item
 
(17 intermediate revisions by 3 users not shown)
Property / describes a project that uses
 
Property / describes a project that uses: ETPS / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: HOL Light / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: LCF / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Coq / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Isabelle/HOL / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Isar / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Isabelle/ZF / 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: ACL2 / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Isabelle/Isar / 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: NQTHM / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Nominal Isabelle / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: Presburger Automata / 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/s10817-009-9157-2 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W2082393912 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4726218 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Termination of term rewriting using dependency pairs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Types for Proofs and Programs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4736387 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Formalizing the Logic-Automaton Connection / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4945200 / 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: Q4435459 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4790656 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Modelling general recursion in type theory / rank
 
Normal rank
Property / cites work
 
Property / cites work: Typed Lambda Calculi and Applications / rank
 
Normal rank
Property / cites work
 
Property / cites work: Computation by Prophecy / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3894958 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4040283 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: A general formulation of simultaneous inductive-recursive definitions in type theory / rank
 
Normal rank
Property / cites work
 
Property / cites work: Partial functions in a total setting / 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: Induction proofs with partial functions / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5287513 / 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: Partial Recursive Functions in Higher-Order Logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Certified Size-Change Termination / rank
 
Normal rank
Property / cites work
 
Property / cites work: Inductive Invariants for Nested Recursion / 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: Deductive synthesis of the unification algorithm / rank
 
Normal rank
Property / cites work
 
Property / cites work: Partial functions in ACL2 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4247084 / 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: Adapting functional programs to higher order logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Verifying the unification algorithm in LCF / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2754066 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Nominal techniques in Isabelle/HOL / rank
 
Normal rank
Property / cites work
 
Property / cites work: On proving the termination of algorithms by machine / rank
 
Normal rank

Latest revision as of 21:19, 2 July 2024

scientific article
Language Label Description Also known as
English
Partial and nested recursive function definitions in higher-order logic
scientific article

    Statements

    Partial and nested recursive function definitions in higher-order logic (English)
    0 references
    0 references
    26 May 2010
    0 references
    0 references
    proof assistants
    0 references
    partial functions
    0 references
    nested recursion
    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
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references