Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Theorem Proving in Higher Order Logics [[electronic resource] ] : 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings / / edited by Jim Grundy, Malcolm Newey
| Theorem Proving in Higher Order Logics [[electronic resource] ] : 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings / / edited by Jim Grundy, Malcolm Newey |
| Edizione | [1st ed. 1998.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
| Descrizione fisica | 1 online resource (IX, 496 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer logic
Artificial intelligence Software engineering Mathematical logic Logic design Logics and Meanings of Programs Artificial Intelligence Software Engineering/Programming and Operating Systems Mathematical Logic and Formal Languages Software Engineering Logic Design |
| ISBN | 3-540-49801-X |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Verified lexical analysis -- Extending window inference -- Program abstraction in a higher-order logic framework -- The village telephone system: A case study in formal software engineering -- Generating embeddings from denotational descriptions -- An interface between CLAM and HOL -- Classical propositional decidability via Nuprl proof extraction -- A comparison of PVS and Isabelle/HOL -- Adding external decision procedures to HOL90 securely -- Formalizing basic first order model theory -- Formalizing Dijkstra -- Mechanical verification of total correctness through diversion verification conditions -- A type annotation scheme for Nuprl -- Verifying a garbage collection algorithm -- Hot: A concurrent automated theorem prover based on higher-order tableaux -- Free variables and subexpressions in higher-order meta logic -- An LPO-based termination ordering for higher-order terms without ?-abstraction -- Proving isomorphism of first-order logic proof systems in HOL -- Exploiting parallelism in interactive theorem provers -- I/O automata and beyond: Temporal logic and abstraction in Isabelle -- Object-oriented verification based on record subtyping in Higher-Order Logic -- On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a high-level synthesis system -- Co-inductive axiomatization of a synchronous language -- Formal specification and theorem proving breakthroughs in geometric modeling -- A tool for data refinement -- Mechanizing relevant logics with HOL -- Case studies in meta-level theorem proving -- Formalization of graph search algorithms and its applications. |
| Record Nr. | UNISA-996466102203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Theorem Proving in Higher Order Logics [[electronic resource] ] : 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings / / edited by Elsa L. Gunter, Amy Felty
| Theorem Proving in Higher Order Logics [[electronic resource] ] : 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings / / edited by Elsa L. Gunter, Amy Felty |
| Edizione | [1st ed. 1997.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
| Descrizione fisica | 1 online resource (X, 346 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Architecture, Computer
Computers Mathematical logic Logic design Software engineering Computer logic Computer System Implementation Theory of Computation Mathematical Logic and Formal Languages Logic Design Software Engineering Logics and Meanings of Programs |
| ISBN | 3-540-69526-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | An Isabelle-based theorem prover for VDM-SL -- Executing formal specifications by translation to higher order logic programming -- Human-style theorem proving using PVS -- A hybrid approach to verifying liveness in a symmetric multi-processor -- Formal verification of concurrent programs in Lp and in Coq: A comparative analysis -- ML programming in constructive type theory -- Possibly infinite sequences in theorem provers: A comparative study -- Proof normalization for a first-order formulation of higher-order logic -- Using a PVS embedding of CSP to verify authentication protocols -- Verifying the accuracy of polynomial approximations in HOL -- A full formalisation of ?-calculus theory in the calculus of constructions -- Rewriting, decision procedures and lemma speculation for automated hardware verification -- Refining reactive systems in HOL using action systems -- On formalization of bicategory theory -- Towards an object-oriented progification language -- Verification for robust specification -- A theory of structured model-based specifications in Isabelle/HOL -- Proof presentation for Isabelle -- Derivation and use of induction schemes in higher-order logic -- Higher order quotients and their implementation in Isabelle HOL -- Type classes and overloading in higher-order logic -- A comparative study of Coq and HOL. |
| Record Nr. | UNINA-9910144919903321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Theorem Proving in Higher Order Logics [[electronic resource] ] : 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings / / edited by Elsa L. Gunter, Amy Felty
| Theorem Proving in Higher Order Logics [[electronic resource] ] : 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings / / edited by Elsa L. Gunter, Amy Felty |
| Edizione | [1st ed. 1997.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
| Descrizione fisica | 1 online resource (X, 346 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Architecture, Computer
Computers Mathematical logic Logic design Software engineering Computer logic Computer System Implementation Theory of Computation Mathematical Logic and Formal Languages Logic Design Software Engineering Logics and Meanings of Programs |
| ISBN | 3-540-69526-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | An Isabelle-based theorem prover for VDM-SL -- Executing formal specifications by translation to higher order logic programming -- Human-style theorem proving using PVS -- A hybrid approach to verifying liveness in a symmetric multi-processor -- Formal verification of concurrent programs in Lp and in Coq: A comparative analysis -- ML programming in constructive type theory -- Possibly infinite sequences in theorem provers: A comparative study -- Proof normalization for a first-order formulation of higher-order logic -- Using a PVS embedding of CSP to verify authentication protocols -- Verifying the accuracy of polynomial approximations in HOL -- A full formalisation of ?-calculus theory in the calculus of constructions -- Rewriting, decision procedures and lemma speculation for automated hardware verification -- Refining reactive systems in HOL using action systems -- On formalization of bicategory theory -- Towards an object-oriented progification language -- Verification for robust specification -- A theory of structured model-based specifications in Isabelle/HOL -- Proof presentation for Isabelle -- Derivation and use of induction schemes in higher-order logic -- Higher order quotients and their implementation in Isabelle HOL -- Type classes and overloading in higher-order logic -- A comparative study of Coq and HOL. |
| Record Nr. | UNISA-996465502503316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Theorem Proving in Higher Order Logics [[electronic resource] ] : 9th International Conference, TPHOLs'96, Turku, Finland, August 26 - 30, 1996, Proceedings / / edited by Joakim von Wright, Jim Grundy, John Harrison
| Theorem Proving in Higher Order Logics [[electronic resource] ] : 9th International Conference, TPHOLs'96, Turku, Finland, August 26 - 30, 1996, Proceedings / / edited by Joakim von Wright, Jim Grundy, John Harrison |
| Edizione | [1st ed. 1996.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 |
| Descrizione fisica | 1 online resource (VIII, 447 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Mathematical logic
Artificial intelligence Logic design Computer logic Software engineering Mathematical Logic and Formal Languages Artificial Intelligence Logic Design Logics and Meanings of Programs Mathematical Logic and Foundations Software Engineering |
| ISBN | 3-540-70641-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Translating specifications in VDM-SL to PVS -- A comparison of HOL and ALF formalizations of a categorical coherence theorem -- Modeling a hardware synthesis methodology in isabelle -- Inference rules for programming languages with side effects in expressions -- Deciding cryptographic protocol adequacy with HOL: The implementation -- Proving liveness of fair transition systems -- Program derivation using the refinement calculator -- A proof tool for reasoning about functional programs -- Coq and hardware verification: A case study -- Elements of mathematical analysis in PVS -- Implementation issues about the embedding of existing high level synthesis algorithms in HOL -- Five axioms of alpha-conversion -- Set theory, higher order logic or both? -- A mizar mode for HOL -- Stålmarck’s algorithm as a HOL derived rule -- Towards applying the composition principle to verify a microkernel operating system -- A modular coding of UNITY in COQ -- Importing mathematics from HOL into Nuprl -- A structure preserving encoding of Z in isabelle/HOL -- Improving the result of high-level synthesis using interactive transformational design -- Using lattice theory in higher order logic -- Formal verification of algorithm W: The monomorphic case -- Verification of compiler correctness for the WAM -- Synthetic domain theory in type theory: Another logic of computable functions -- Function definition in higher-order logic -- Higher-order annotated terms for proof search -- A comparison of MDG and HOL for hardware verification -- A mechanisation of computability theory in HOL. |
| Record Nr. | UNISA-996465954203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Types for Proofs and Programs [[electronic resource] ] : International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers / / edited by Stefano Berardi, Mario Coppo, Ferruccio Damiani
| Types for Proofs and Programs [[electronic resource] ] : International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers / / edited by Stefano Berardi, Mario Coppo, Ferruccio Damiani |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (X, 412 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Programming languages (Electronic computers)
Computer logic Mathematical logic Artificial intelligence Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence |
| ISBN |
3-540-24849-8
3-540-22164-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | A Modular Hierarchy of Logical Frameworks -- Tailoring Filter Models -- Locales and Locale Expressions in Isabelle/Isar -- to PAF!, a Proof Assistant for ML Programs Verification -- A Constructive Proof of Higman’s Lemma in Isabelle -- A Core Calculus of Higher-Order Mixins and Classes -- Type Inference for Nested Self Types -- Inductive Families Need Not Store Their Indices -- Modules in Coq Are and Will Be Correct -- Rewriting Calculus with Fixpoints: Untyped and First-Order Systems -- First-Order Reasoning in the Calculus of Inductive Constructions -- Higher-Order Linear Ramified Recurrence -- Confluence and Strong Normalisation of the Generalised Multiary ?-Calculus -- Wellfounded Trees and Dependent Polynomial Functors -- Classical Proofs, Typed Processes, and Intersection Types -- “Wave-Style” Geometry of Interaction Models in Rel Are Graph-Like Lambda-Models -- Coercions in Hindley-Milner Systems -- Combining Incoherent Coercions for ? -Types -- Induction and Co-induction in Sequent Calculus -- QArith: Coq Formalisation of Lazy Rational Arithmetic -- Mobility Types in Coq -- Some Algebraic Structures in Lambda-Calculus with Inductive Types -- A Concurrent Logical Framework: The Propositional Fragment -- Formal Proof Sketches -- Applied Type System. |
| Record Nr. | UNISA-996465431103316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Types for Proofs and Programs : International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers / / edited by Stefano Berardi, Mario Coppo, Ferruccio Damiani
| Types for Proofs and Programs : International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers / / edited by Stefano Berardi, Mario Coppo, Ferruccio Damiani |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (X, 412 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Programming languages (Electronic computers)
Computer logic Mathematical logic Artificial intelligence Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence |
| ISBN |
3-540-24849-8
3-540-22164-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | A Modular Hierarchy of Logical Frameworks -- Tailoring Filter Models -- Locales and Locale Expressions in Isabelle/Isar -- to PAF!, a Proof Assistant for ML Programs Verification -- A Constructive Proof of Higman’s Lemma in Isabelle -- A Core Calculus of Higher-Order Mixins and Classes -- Type Inference for Nested Self Types -- Inductive Families Need Not Store Their Indices -- Modules in Coq Are and Will Be Correct -- Rewriting Calculus with Fixpoints: Untyped and First-Order Systems -- First-Order Reasoning in the Calculus of Inductive Constructions -- Higher-Order Linear Ramified Recurrence -- Confluence and Strong Normalisation of the Generalised Multiary ?-Calculus -- Wellfounded Trees and Dependent Polynomial Functors -- Classical Proofs, Typed Processes, and Intersection Types -- “Wave-Style” Geometry of Interaction Models in Rel Are Graph-Like Lambda-Models -- Coercions in Hindley-Milner Systems -- Combining Incoherent Coercions for ? -Types -- Induction and Co-induction in Sequent Calculus -- QArith: Coq Formalisation of Lazy Rational Arithmetic -- Mobility Types in Coq -- Some Algebraic Structures in Lambda-Calculus with Inductive Types -- A Concurrent Logical Framework: The Propositional Fragment -- Formal Proof Sketches -- Applied Type System. |
| Record Nr. | UNINA-9910144152703321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Types for Proofs and Programs [[electronic resource] ] : International Workshop TYPES'96, Aussois, France, December 15-19, 1996 Selected Papers / / edited by Eduardo Gimenez, Christine Paulin-Mohring
| Types for Proofs and Programs [[electronic resource] ] : International Workshop TYPES'96, Aussois, France, December 15-19, 1996 Selected Papers / / edited by Eduardo Gimenez, Christine Paulin-Mohring |
| Edizione | [1st ed. 1998.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
| Descrizione fisica | 1 online resource (VIII, 380 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computer logic Mathematical logic Programming languages (Electronic computers) Artificial intelligence Software Engineering/Programming and Operating Systems Logics and Meanings of Programs Mathematical Logic and Formal Languages Programming Languages, Compilers, Interpreters Artificial Intelligence |
| ISBN | 3-540-49562-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Coercion synthesis in computer implementations of type-theoretic frameworks -- Verification of the interface of a small proof system in coq -- An implementation of the Heine-Borel covering theorem in type theory -- Detecting and removing dead-code using rank 2 intersection -- A type-free formalization of mathematics where proofs are objects -- Higman's lemma in type theory -- A proof of weak termination of typed ??-calculi -- Proof style -- Some algorithmic and proof-theoretical aspects of coercive subtyping -- Semantical BNF -- The internal type theory of a Heyting pretopos -- Inverting inductively defined relations in LEGO -- A generic normalisation proof for pure type systems -- Proving a real time algorithm for ATM in Coq -- Dependent types with explicit substitutions: A meta-theoretical development -- Type inference verified: Algorithm W in Isabelle/HOL -- Continuous lattices in formal topology -- Abstract insertion sort in an extension of type theory with record types and subtyping. |
| Record Nr. | UNINA-9910144122303321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Types for Proofs and Programs [[electronic resource] ] : International Workshop TYPES'96, Aussois, France, December 15-19, 1996 Selected Papers / / edited by Eduardo Gimenez, Christine Paulin-Mohring
| Types for Proofs and Programs [[electronic resource] ] : International Workshop TYPES'96, Aussois, France, December 15-19, 1996 Selected Papers / / edited by Eduardo Gimenez, Christine Paulin-Mohring |
| Edizione | [1st ed. 1998.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
| Descrizione fisica | 1 online resource (VIII, 380 p.) |
| Disciplina | 004/.01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computer logic Mathematical logic Programming languages (Electronic computers) Artificial intelligence Software Engineering/Programming and Operating Systems Logics and Meanings of Programs Mathematical Logic and Formal Languages Programming Languages, Compilers, Interpreters Artificial Intelligence |
| ISBN | 3-540-49562-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Coercion synthesis in computer implementations of type-theoretic frameworks -- Verification of the interface of a small proof system in coq -- An implementation of the Heine-Borel covering theorem in type theory -- Detecting and removing dead-code using rank 2 intersection -- A type-free formalization of mathematics where proofs are objects -- Higman's lemma in type theory -- A proof of weak termination of typed ??-calculi -- Proof style -- Some algorithmic and proof-theoretical aspects of coercive subtyping -- Semantical BNF -- The internal type theory of a Heyting pretopos -- Inverting inductively defined relations in LEGO -- A generic normalisation proof for pure type systems -- Proving a real time algorithm for ATM in Coq -- Dependent types with explicit substitutions: A meta-theoretical development -- Type inference verified: Algorithm W in Isabelle/HOL -- Continuous lattices in formal topology -- Abstract insertion sort in an extension of type theory with record types and subtyping. |
| Record Nr. | UNISA-996465945603316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
