SwePub
Sök i SwePub databas

  Utökad sökning

Träfflista för sökning "L773:9783642396335 "

Sökning: L773:9783642396335

  • Resultat 1-2 av 2
Sortera/gruppera träfflistan
   
NumreringReferensOmslagsbildHitta
1.
  • Armstrong, Alasdair, et al. (författare)
  • Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
  • 2013
  • Ingår i: Interactive Theorem Proving. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642396335 ; , s. 197-212
  • Konferensbidrag (refereegranskat)abstract
    • Schematic Kleene algebra with tests (SKAT) supports the equational verification of flowchart scheme equivalence and captures simple while-programs with assignment statements. We formalise SKAT in Isabelle/HOL, using the quotient type package to reason equationally in this algebra. We apply this formalisation to a complex flowchart transformation proof from the literature. We extend SKAT with assertion statements and derive the inference rules of Hoare logic. We apply this extension in simple program verification examples and the derivation of additional Hoare-style rules. This shows that algebra can provide an abstract semantic layer from which different program analysis and verification tasks can be implemented in a simple lightweight way.
  •  
2.
  • Cohen, Cyril, 1985 (författare)
  • Pragmatic Quotient Types in Coq
  • 2013
  • Ingår i: Lecture Notes in Computer Science. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 0302-9743. - 9783642396335 ; 7998, s. 213-228
  • Konferensbidrag (refereegranskat)abstract
    • In intensional type theory, it is not always possible to form the quotient of a type by an equivalence relation. However, quotients are extremely useful when formalizing mathematics, especially in algebra. We provide a Coq library with a pragmatic approach in two complementary components. First, we provide a framework to work with quotient types in an axiomatic manner. Second, we program construction mechanisms for some specific cases where it is possible to build a quotient type. This library was helpful in implementing the types of rational fractions, multivariate polynomials, field extensions and real algebraic numbers.
  •  
Skapa referenser, mejla, bekava och länka
  • Resultat 1-2 av 2
Typ av publikation
konferensbidrag (2)
Typ av innehåll
refereegranskat (2)
Författare/redaktör
Armstrong, Alasdair (1)
Struth, Georg (1)
Weber, Tjark (1)
Cohen, Cyril, 1985 (1)
Lärosäte
Göteborgs universitet (1)
Uppsala universitet (1)
Språk
Engelska (2)
Forskningsämne (UKÄ/SCB)
Naturvetenskap (2)
År
2013 (2)

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.

 
pil uppåt Stäng

Kopiera och spara länken för att återkomma till aktuell vy