9 found
Sort by:
Disambiguations:
Robert Boyer [8]Robert S. Boyer [1]
  1. Robert S. Boyer & J. Strother Moore, Program Verification.
    How are the properties of computer programs proved? We discuss three approaches in this article: inductive invariants, functional semantics, and explicit semantics. Because the first approach has received by far the most attention, it has produced the most impressive results to date. However, the field is now moving away from the inductive invariant approach.
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  2. Robert Boyer, A Mechanical Proof of the Unsolvability of the Halting Problem.
    We describe a proof by a computer program of the unsolvability of the halting problem. The halting problem is posed in a constructive, formal language. The computational paradigm formalized is Pure LISP, not Turing machines. The machine was led to the proof by the authors, who suggested certain function definitions and stated certain intermediate lemmas. The machine checked that every suggested definition was admissible and the machine proved the main theorem and every lemma. We believe this is the first instance (...)
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  3. Robert Boyer, Metafunctions in Nqthm and Acl.
    Meta-level reasoning was added to the Boyer-Moore theorem prover by 1979. We have recently re-implemented and, we think, slightly improved our approach to meta-theoretic reasoning in the Acl2 theorem prover. However, there is lots of room for much more substantial improvement. Our talk will consist of 3 parts: review, recent results, and general remarks.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  4. Robert Boyer, Proof Checking the Rsa Public Key Encryption Algorithm.
    The development of mathematics toward greater precision has led, as is well known, to the formalization of large tracts of it, so that one can prove any theorem using nothing but a few mechanical rules. -- Godel [11].
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  5. Robert Boyer, The Addition of Bounded Quantification and Partial Functions to a Computational Logic and its Theorem Prover.
    We describe an extension to our quantifier-free computational logic to provide the expressive power and convenience of bounded quantifiers and partial functions. By quantifier we mean a formal construct which introduces a bound or indicial variable whose scope is some subexpression of the quantifier expression. A familiar quantifier is the Σ operator which sums the values of an expression over some range of values on the bound variable. Our method is to represent expressions of the logic as objects in the (...)
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  6. Robert Boyer, The Use of a Formal Simulator to Verify a Simple Real Time Control Program.
    We present an initial and elementary investigation of the formal specification and mechanical verification of programs that interact with environments. We describe a formal, mechanically produced proof that a simple, real time control program keeps a vehicle on a straightline course in a variable crosswind. To formalize the specification we define a mathematical function which models the interaction of the program and its environment. We then state and prove two theorems about this function: the simulated vehicle never gets farther than (...)
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  7. Robert Boyer (2002). What Institutional Regimes for the Era of Internationalization? In Yves Dezalay & Bryant G. Garth (eds.), Global Prescriptions: The Production, Exportation, and Importation of a New Legal Orthodoxy. University of Michigan Press.
     
    My bibliography  
     
    Export citation  
  8. Robert Boyer (1998). The Pyrrhic Victory of Anglo-Saxon Capitalism. Thesis Eleven 53 (1):93-101.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  9. Robert Boyer (1995). La Théorie de la Régulation Dans les Années 1990. Actuel Marx 17:19-38.
    No categories
     
    My bibliography  
     
    Export citation