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.
Interactive Theorem Proving [[electronic resource] ] : 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013, Proceedings / / edited by Sandrine Blazy, Christine Paulin-Mohring, David Pichardie
| Interactive Theorem Proving [[electronic resource] ] : 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013, Proceedings / / edited by Sandrine Blazy, Christine Paulin-Mohring, David Pichardie |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XII, 498 p. 73 illus.) |
| Disciplina | 004.015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Artificial intelligence Computer science Software engineering Data protection Algorithms Formal Languages and Automata Theory Artificial Intelligence Computer Science Logic and Foundations of Programming Software Engineering Data and Information Security |
| ISBN | 3-642-39634-8 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Applying Formal Methods in the Large -- Automating Theorem Proving with SMT -- Certifying Voting Protocols -- Invited Tutorials.-Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities -- Canonical Structures for the Working Coq User -- Regular Papers -- MaSh: Machine Learning for Sledgehammer -- Scalable LCF-Style Proof Translation -- Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation -- Automatic Data Refinement -- Data Refinement in Isabelle/HOL -- Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable -- Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω1 -- Mechanising Turing Machines and Computability Theory in Isabelle/HOL.-A Machine-Checked Proof of the Odd Order Theorem -- Kleene Algebra with Tests and Coq Tools for while Programs.-Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL -- Pragmatic Quotient Types in Coq -- Mechanical Verification of SAT Refutations with Extended Resolution -- Formalizing Bounded Increase -- Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types -- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL -- Formal Reasoning about Classified Markov Chains in HOL -- Practical Probability: Applying pGCL to Lattice Scheduling -- Adjustable References -- Handcrafted Inversions Made Operational on Operational Semantics -- Circular Coinduction in Coq Using Bisimulation-Up-To Techniques -- Program Extraction from Nested Definitions -- Subformula Linking as an Interaction Method -- Automatically Generated Infrastructure for De Bruijn Syntaxes -- Shared-Memory Multiprocessing for Interactive Theorem Proving -- A Parallelized Theorem Prover for a Logic with Parallel Execution -- Rough Diamonds -- Communicating Formal Proofs: The Case of Flyspeck -- Square Root and Division Elimination in PVS -- The Picard Algorithm for Ordinary Differential Equations in Coq -- Stateless Higher-Order Logic with Quantified Types -- Implementing Hash-Consed Structures in Coq -- Towards Certifying Network Calculus -- Steps towards Verified Implementations of HOL Light. |
| Record Nr. | UNISA-996465982703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Interactive Theorem Proving : 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013, Proceedings / / edited by Sandrine Blazy, Christine Paulin-Mohring, David Pichardie
| Interactive Theorem Proving : 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013, Proceedings / / edited by Sandrine Blazy, Christine Paulin-Mohring, David Pichardie |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XII, 498 p. 73 illus.) |
| Disciplina | 004.015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Artificial intelligence Computer science Software engineering Data protection Algorithms Formal Languages and Automata Theory Artificial Intelligence Computer Science Logic and Foundations of Programming Software Engineering Data and Information Security |
| ISBN | 3-642-39634-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Applying Formal Methods in the Large -- Automating Theorem Proving with SMT -- Certifying Voting Protocols -- Invited Tutorials.-Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities -- Canonical Structures for the Working Coq User -- Regular Papers -- MaSh: Machine Learning for Sledgehammer -- Scalable LCF-Style Proof Translation -- Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation -- Automatic Data Refinement -- Data Refinement in Isabelle/HOL -- Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable -- Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω1 -- Mechanising Turing Machines and Computability Theory in Isabelle/HOL.-A Machine-Checked Proof of the Odd Order Theorem -- Kleene Algebra with Tests and Coq Tools for while Programs.-Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL -- Pragmatic Quotient Types in Coq -- Mechanical Verification of SAT Refutations with Extended Resolution -- Formalizing Bounded Increase -- Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types -- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL -- Formal Reasoning about Classified Markov Chains in HOL -- Practical Probability: Applying pGCL to Lattice Scheduling -- Adjustable References -- Handcrafted Inversions Made Operational on Operational Semantics -- Circular Coinduction in Coq Using Bisimulation-Up-To Techniques -- Program Extraction from Nested Definitions -- Subformula Linking as an Interaction Method -- Automatically Generated Infrastructure for De Bruijn Syntaxes -- Shared-Memory Multiprocessing for Interactive Theorem Proving -- A Parallelized Theorem Prover for a Logic with Parallel Execution -- Rough Diamonds -- Communicating Formal Proofs: The Case of Flyspeck -- Square Root and Division Elimination in PVS -- The Picard Algorithm for Ordinary Differential Equations in Coq -- Stateless Higher-Order Logic with Quantified Types -- Implementing Hash-Consed Structures in Coq -- Towards Certifying Network Calculus -- Steps towards Verified Implementations of HOL Light. |
| Record Nr. | UNINA-9910483676803321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Mathematics of Program Construction [[electronic resource] ] : 9th International Conference, MPC 2008 Marseille, France, July 15-18, 2008 Proceedings / / edited by Philippe Audebaud, Christine Paulin-Mohring
| Mathematics of Program Construction [[electronic resource] ] : 9th International Conference, MPC 2008 Marseille, France, July 15-18, 2008 Proceedings / / edited by Philippe Audebaud, Christine Paulin-Mohring |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 |
| Descrizione fisica | 1 online resource (X, 423 p.) |
| Disciplina | 005.11 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer programming
Software engineering Compilers (Computer programs) Computer science Machine theory Programming Techniques Software Engineering Compilers and Interpreters Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory |
| ISBN | 3-540-70594-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Exploiting Unique Fixed Points -- Scrap Your Type Applications -- Programming with Effects in Coq -- Verifying a Semantic ??-Conversion Test for Martin-Löf Type Theory -- The Capacity-C Torch Problem -- Recounting the Rationals: Twice! -- Zippy Tabulations of Recursive Functions -- Unfolding Abstract Datatypes -- Circulations, Fuzzy Relations and Semirings -- Asynchronous Exceptions as an Effect -- The Böhm–Jacopini Theorem Is False, Propositionally -- The Expression Lemma -- Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening -- Probabilistic Choice in Refinement Algebra -- Algebra of Programming Using Dependent Types -- Safe Modification of Pointer Programs in Refinement Calculus -- A Hoare Logic for Call-by-Value Functional Programs -- Synthesis of Optimal Control Policies for Some Infinite-State Transition Systems -- Modal Semirings Revisited -- Asymptotic Improvement of Computations over Free Monads -- Symmetric and Synchronous Communication in Peer-to-Peer Networks. |
| Record Nr. | UNISA-996465840003316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Types for Proofs and Programs [[electronic resource] ] : International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers / / edited by Jean-Christophe Filliatre, Christine Paulin-Mohring, Benjamin Werner
| Types for Proofs and Programs [[electronic resource] ] : International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers / / edited by Jean-Christophe Filliatre, Christine Paulin-Mohring, Benjamin Werner |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 |
| Descrizione fisica | 1 online resource (VIII, 280 p.) |
| Disciplina | 005.131 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Compilers (Computer programs) Machine theory Computer science—Mathematics Artificial intelligence Computer Science Logic and Foundations of Programming Compilers and Interpreters Formal Languages and Automata Theory Symbolic and Algebraic Manipulation Artificial Intelligence |
| ISBN | 3-540-31429-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Formalized Metatheory with Terms Represented by an Indexed Family of Types -- A Content Based Mathematical Search Engine: Whelp -- A Machine-Checked Formalization of the Random Oracle Model -- Extracting a Normalization Algorithm in Isabelle/HOL -- A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis -- Formalising Bitonic Sort in Type Theory -- A Semi-reflexive Tactic for (Sub-)Equational Reasoning -- A Uniform and Certified Approach for Two Static Analyses -- Solving Two Problems in General Topology Via Types -- A Tool for Automated Theorem Proving in Agda -- Surreal Numbers in Coq -- A Few Constructions on Constructors -- Tactic-Based Optimized Compilation of Functional Programs -- Interfaces as Games, Programs as Strategies -- ?Z: Zermelo’s Set Theory as a PTS with 4 Sorts -- Exploring the Regular Tree Types -- On Constructive Existence. |
| Record Nr. | UNISA-996466114703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
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 | ||
| ||