Search results for "isabelle"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
100	David C. J. Matthews, Makarius Wenzel	Efficient parallel programming in Poly/ML and Isabelle/ML.	DAMP	2010	DBLP DOI BibTeX RDF	parallel standard ml, poly/ml, theorem proving applications, data parallelism, isabelle
90	Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow	The Isabelle Framework.	TPHOLs	2008	DBLP DOI BibTeX RDF
79	Graeme Smith 0001, Florian Kammüller, Thomas Santen	Encoding Object-Z in Isabelle/HOL.	ZB	2002	DBLP DOI BibTeX RDF	reference semantics, Object-Z, higher-order logic, Isabelle
69	Steven Obua, Sebastian Skalberg	Importing HOL into Isabelle/HOL.	IJCAR	2006	DBLP DOI BibTeX RDF
62	Florian Haftmann	From higher-order logic to Haskell: there and back again.	PEPM	2010	DBLP DOI BibTeX RDF	code generation, theorem proving, haskell, higher-order logic, isabelle
59	Makarius Wenzel, Burkhart Wolff	Building Formal Method Tools in the Isabelle/Isar Framework.	TPHOLs	2007	DBLP DOI BibTeX RDF
59	Sean McLaughlin	An Interpretation of Isabelle/HOL in HOL Light.	IJCAR	2006	DBLP DOI BibTeX RDF
59	Tobias Nipkow, Lawrence C. Paulson	Isabelle-91.	CADE	1992	DBLP DOI BibTeX RDF
57	Lawrence C. Paulson	Mechanizing UNITY in Isabelle.	ACM Trans. Comput. Log.	2000	DBLP DOI BibTeX RDF	concurrency, UNITY, Isabelle, compositional reasoning
48	Alexander Schimpf, Stephan Merz, Jan-Georg Smaus	Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL.	TPHOLs	2009	DBLP DOI BibTeX RDF
48	Robert Lamar, Fairouz Kamareddine, J. B. Wells	MathLang Translation to Isabelle Syntax.	Calculemus/MKM	2009	DBLP DOI BibTeX RDF
48	Markus Wenzel 0001, Lawrence C. Paulson	Isabelle/Isar.	The Seventeen Provers of the World	2006	DBLP DOI BibTeX RDF
48	Florian Haftmann, Makarius Wenzel	Constructive Type Classes in Isabelle.	TYPES	2006	DBLP DOI BibTeX RDF
48	Clemens Ballarin	Interpretation of Locales in Isabelle: Theories and Proof Contexts.	MKM	2006	DBLP DOI BibTeX RDF
48	Sergey Tverdyshev	Combination of Isabelle/HOL with Automatic Tools.	FroCoS	2005	DBLP DOI BibTeX RDF
48	Florian Kammüller, Jeff W. Sanders	Idempotent Relations in Isabelle/HOL.	ICTAC	2004	DBLP DOI BibTeX RDF
48	Yue Tang, Jin Song Dong, Jing Sun 0002, Brendan P. Mahony	Reasoning about Semantic Web in Isabelle/HOL.	APSEC	2004	DBLP DOI BibTeX RDF
48	Mark Staples	Representing WP Semantics in Isabelle/ZF.	TPHOLs	1999	DBLP DOI BibTeX RDF
48	Olaf Müller	I/O Automata and Beyond: Temporal Logic and Abstraction in Isabelle.	TPHOLs	1998	DBLP DOI BibTeX RDF
48	Oscar Slotosch	Higher Order Quotients and their Implementation in Isabelle HOL.	TPHOLs	1997	DBLP DOI BibTeX RDF
48	Haykal Tej, Burkhart Wolff	A Corrected Failure Divergence Model for CSP in Isabelle/HOL.	FME	1997	DBLP DOI BibTeX RDF
48	Sara Kalvala	A Formulation of TLA in Isabelle.	TPHOLs	1995	DBLP DOI BibTeX RDF
47	Markus Kaiser 0002, Ralf Lämmel	An Isabelle/HOL-based model of stratego-like traversal strategies.	PPDP	2009	DBLP DOI BibTeX RDF	generic functional programming, traversal strategies, domain specific languages, rewriting, isabelle/hol, software transformation, stratego
47	Peter Chapman, James McKinna, Christian Urban	Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle.	AISC/MKM/Calculemus	2008	DBLP DOI BibTeX RDF	Nominal Isabelle, logic, automated reasoning, Formal mathematics
47	William Billingsley, Peter Robinson 0001	Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	Intelligent book, MathsTiles, Isabelle
47	Achim D. Brucker, Burkhart Wolff	A Proposal for a Formal OCL Semantics in Isabelle/HOL.	TPHOLs	2002	DBLP DOI BibTeX RDF	shallow embedding, UML, testing, OCL, Isabelle
47	Sidi O. Ehmety, Lawrence C. Paulson	Program Composition in Isabelle/UNITY.	IPDPS	2002	DBLP DOI BibTeX RDF	program composition, universal and existential properties, UNITY, Isabelle
42	Damián Barsotti, Leonor Prensa Nieto, Alwen Tiu	Verification of clock synchronization algorithms: experiments on a combination of deductive tools.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Combination of deductive tools, Verification, Theorem proving, Clock synchronization
41	Sabine Glesner, Jan Olaf Blech	Coalgebraic Semantics for Component Systems.	Architecting Systems with Trustworthy Components	2004	DBLP DOI BibTeX RDF	verification, semantics, Components, Isabelle/HOL, coinduction, component interaction
41	David von Oheimb, Tobias Nipkow	Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited.	FME	2002	DBLP DOI BibTeX RDF	Java, Hoare logic, side effects, dynamic binding, Isabelle/HOL, auxiliary variables
41	David von Oheimb	Hoare Logic for Mutual Recursion and Local Variables.	FSTTCS	1999	DBLP DOI BibTeX RDF	axiomaticsemantics, relative completeness, local variables, call-by-value parameters, soundness, Hoare logic, Isabelle/HOL, mutual recursion
41	David von Oheimb, Thomas F. Gritzner	RALL: Machine-Supported Proofs for Relation Algebra.	CADE	1997	DBLP DOI BibTeX RDF	interactive and automatic theorem proving, atom structure, Relation algebra, Isabelle
37	Andreas Lochbihler	Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL.	TPHOLs	2009	DBLP DOI BibTeX RDF
37	Florian Haftmann, Makarius Wenzel	Local Theory Specifications in Isabelle/Isar.	TYPES	2008	DBLP DOI BibTeX RDF
37	Stefan Berghofer, Makarius Wenzel	Logic-Free Reasoning in Isabelle/Isar.	AISC/MKM/Calculemus	2008	DBLP DOI BibTeX RDF
37	Steven Obua	Partizan Games in Isabelle/HOLZF.	ICTAC	2006	DBLP DOI BibTeX RDF
37	Steven Obua	Proving Bounds for Real Linear Programs in Isabelle/HOL.	TPHOLs	2005	DBLP DOI BibTeX RDF
37	Jan Olaf Blech, Lars Gesellensetter, Sabine Glesner	Formal Verification of Dead Code Elimination in Isabelle/HOL.	SEFM	2005	DBLP DOI BibTeX RDF
37	Daniel Hausmann 0001, Till Mossakowski, Lutz Schröder	Iterative Circular Coinduction for CoCasl in Isabelle/HOL.	FASE	2005	DBLP DOI BibTeX RDF
37	Stefan Berghofer	Extracting a Normalization Algorithm in Isabelle/HOL.	TYPES	2004	DBLP DOI BibTeX RDF
37	Laura I. Meikle, Jacques D. Fleuriot	Formalizing Hilbert's Grundlagen in Isabelle/Isar.	TPHOLs	2003	DBLP DOI BibTeX RDF
37	Helko Lehmann, Michael Leuschel	Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce.	LOPSTR	2003	DBLP DOI BibTeX RDF
37	Simon J. Gay	A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL.	TPHOLs	2001	DBLP DOI BibTeX RDF	semantics, Types, pi calculus, automatic theorem proving
37	Gertrud Bauer, Markus Wenzel 0001	Calculational Reasoning Revisited (An Isabelle/Isar Experience).	TPHOLs	2001	DBLP DOI BibTeX RDF
37	Christine Röckl, Daniel Hirschkoff, Stefan Berghofer	Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts.	FoSSaCS	2001	DBLP DOI BibTeX RDF
37	Leonor Prensa Nieto, Javier Esparza	Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL.	MFCS	2000	DBLP DOI BibTeX RDF
37	Florian Kammüller	Modular Reasoning in Isabelle.	CADE	2000	DBLP DOI BibTeX RDF
37	Gertrud Bauer, Markus Wenzel 0001	Computer-Assisted Mathematics at Work (The Hahn-Banach Theorem in Isabelle/Isar).	TYPES	1999	DBLP DOI BibTeX RDF
37	Cornelia Pusch	Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL.	TACAS	1999	DBLP DOI BibTeX RDF
37	W. O. David Griffioen, Marieke Huisman	A Comparison of PVS and Isabelle/HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
37	Florian Kammüller	Modular Structures as Dependent Types in Isabelle.	TYPES	1998	DBLP DOI BibTeX RDF
37	Pierre Chartier	Formalisation of B in Isabelle/HOL.	B	1998	DBLP DOI BibTeX RDF
37	Thomas Santen	A Theory of Structured Model-Based Specifications in Isabelle/HOL.	TPHOLs	1997	DBLP DOI BibTeX RDF
37	Tobias Nipkow	More Church-Rosser Proofs (in Isabelle/HOL).	CADE	1996	DBLP DOI BibTeX RDF
37	Ole Rasmussen	An Embedding of Ruby in Isabelle.	CADE	1996	DBLP DOI BibTeX RDF
37	Sten Agerholm, Michael J. C. Gordon	Experiments with ZF Set Theory in HOL and Isabelle.	TPHOLs	1995	DBLP DOI BibTeX RDF
37	Lawrence C. Paulson	A formulation of the simple theory of types (for Isabelle).	Conference on Computer Logic	1988	DBLP DOI BibTeX RDF
33	Hao Xu, Yongwang Zhao	Isabelle/Cloud: Delivering Isabelle/HOL as a Cloud IDE for Theorem Proving.	Internetware	2023	DBLP DOI BibTeX RDF
33	Achim D. Brucker	Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML.	Arch. Formal Proofs	2022	DBLP BibTeX RDF
33	Diego Marmsoler, Achim D. Brucker	Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL.	Arch. Formal Proofs	2022	DBLP BibTeX RDF
33	Joshua Chen	Isabelle/Spartan - A Dependent Type Theory Framework for Isabelle.	CoRR	2020	DBLP BibTeX RDF
33	Albert Rizaldi	Formal specification, monitoring, and verification of autonomous vehicles in Isabelle/HOL (Formale Spezifikation, Erfüllbarkeitsanalyse, und formale Verifikation von autonomen Fahrzeugen in Isabelle/HOL) (PDF / PS)		2020	RDF
33	Makarius Wenzel	Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit.	UITP	2010	DBLP DOI BibTeX RDF
32	Stefan Berghofer, Lukas Bulwahn, Florian Haftmann	Turning Inductive into Equational Specifications.	TPHOLs	2009	DBLP DOI BibTeX RDF
32	René Thiemann, Christian Sternagel	Certification of Termination Proofs Using CeTA.	TPHOLs	2009	DBLP DOI BibTeX RDF
32	Lawrence C. Paulson, Kong Woei Susanto	Source-Level Proof Reconstruction for Interactive Theorem Proving.	TPHOLs	2007	DBLP DOI BibTeX RDF
32	Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu	Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants.	TACAS	2006	DBLP DOI BibTeX RDF
32	Steffen Helke, Florian Kammüller	Structure Preserving Data Abstractions for Statecharts.	FORTE	2005	DBLP DOI BibTeX RDF
32	Dirk Leinenbach, Wolfgang J. Paul, Elena Petrova	Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes.	SEFM	2005	DBLP DOI BibTeX RDF
32	Stefan Berghofer	Program Extraction in Simply-Typed Higher Order Logic.	TYPES	2002	DBLP DOI BibTeX RDF
32	Jeremy E. Dawson, Rajeev Goré	A Mechanised Proof System for Relation Algebra using Display Logic.	JELIA	1998	DBLP DOI BibTeX RDF
31	Matthias Daum 0001, Jan Dörrenbächer, Burkhart Wolff	Proving Fairness and Implementation Correctness of a Microkernel Scheduler.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Formal verification, Interactive theorem proving, Microkernel, Isabelle/HOL
31	Gerwin Klein, Philip Derrin, Kevin Elphinstone	Experience report: seL4: formally verifying a high-performance microkernel.	ICFP	2009	DBLP DOI BibTeX RDF	seL4, haskell, microkernel, Isabelle/HOL
31	Jesús Aransay, Clemens Ballarin, Julio Rubio 0001	A Mechanized Proof of the Basic Perturbation Lemma.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Homological algebra, Basic perturbation lemma, Isabelle
31	Nik Sultana, Simon J. Thompson	Mechanical verification of refactorings.	PEPM	2008	DBLP DOI BibTeX RDF	refactoring, Isabelle/HOL
31	Achim D. Brucker, Burkhart Wolff	Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing.	TAP	2007	DBLP DOI BibTeX RDF	symbolic test case generations, theorem proving, computer security, black box testing, Isabelle/HOL, test sequence generation
31	Giampaolo Bella, Lawrence C. Paulson	Accountability protocols: Formalized and verified.	ACM Trans. Inf. Syst. Secur.	2006	DBLP DOI BibTeX RDF	inductive method, proof tools, Isabelle, Nonrepudiation, certified email
31	Giampaolo Bella, Fabio Massacci, Lawrence C. Paulson	Verifying the SET Purchase Protocols.	J. Autom. Reason.	2006	DBLP DOI BibTeX RDF	deductive verification, electronic commerce, security protocols, Isabelle, inductive definitions
31	Sabine Glesner	Finite Integer Computations: An Algebraic Foundation for Their Correctness.	Formal Aspects Comput.	2006	DBLP DOI BibTeX RDF	Additional Keywords finite integer and residue class arithmetic, changing representation sizes, Java Card bytecode optimization, constant folding, Java and C arithmetic, formal verification, inconsistency, Java Card, Isabelle/HOL
31	David von Oheimb, Volkmar Lotz, Georg Walter	Analyzing SLE 88 memory management security using Interacting State Machines.	Int. J. Inf. Sec.	2005	DBLP DOI BibTeX RDF	Security, Smart cards, Memory management, Formal analysis, Isabelle/HOL
31	Sidi O. Ehmety, Lawrence C. Paulson	Mechanizing compositional reasoning for concurrent systems: some lessons.	Formal Aspects Comput.	2005	DBLP DOI BibTeX RDF	Existential properties, Universal properties, Guarantees assertions, UNITY, Isabelle, Compositional reasoning
31	Lawrence C. Paulson	Organizing Numerical Theories Using Axiomatic Type Classes.	J. Autom. Reason.	2004	DBLP DOI BibTeX RDF	axiomatic type classes, polymorphism, arithmetic, overloading, Isabelle
31	Gerwin Klein, Martin Wildmoser	Verified Bytecode Subroutines.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	Java, theorem proving, subroutines, dataflow analysis, Isabelle, bytecode verification
31	S. J. Ambler, Roy L. Crole, Alberto Momigliano	A definitional approach to primitivexs recursion over higher order abstract syntax.	MERLIN	2003	DBLP DOI BibTeX RDF	Isabelle HOL, topos theory, ?-calculus, higher order abstract syntax, primitive recursion, initial algebras
31	Giampaolo Bella, Lawrence C. Paulson, Fabio Massacci	The verification of an industrial payment protocol: the SET purchase phase.	CCS	2002	DBLP DOI BibTeX RDF	inductive specifications, isabelle proof assistant, formal verification, electronic commerce, security protocols
31	Lawrence C. Paulson	Mechanizing a theory of program composition for UNITY.	ACM Trans. Program. Lang. Syst.	2001	DBLP DOI BibTeX RDF	concurrency, UNITY, Isabelle, compositional reasoning
31	Lawrence C. Paulson	Inductive Analysis of the Internet Protocol TLS.	ACM Trans. Inf. Syst. Secur.	1999	DBLP DOI BibTeX RDF	inductive method, proof tools, authentication, TLS, Isabelle
31	Lawrence C. Paulson	Mechanized proofs for a recursive authentication protocol.	CSFW	1997	DBLP DOI BibTeX RDF	mechanized proofs, recursive authentication protocol, inductive approach, message nesting, basic security theorem, adjacent pairs, honest agents, protocol complexity, agents, protocols, specification, symmetry, mutual authentication, Isabelle/HOL, session keys
30	Ziqi Zhang 0001, Anna Lisa Gentile, Isabelle Augenstein	"Linked data as background knowledge for information extraction on the web" by Ziqi Zhang, Anna Lisa Gentile and Isabelle Augenstein with Martin Vesely as coordinator.	SIGWEB Newsl.	2014	DBLP DOI BibTeX RDF
28	Antoine Boutier, Isabelle Martinez, Isabelle Daniel, Simone Tumiati, Guillaume Siron, Alberto Vitale Brovarone	Thermotopes-COH - A software for carbon isotope modeling and speciation of COH fluids.	Comput. Geosci.	2024	DBLP DOI BibTeX RDF
28	Emmanuel Chemla, Isabelle Charnavel, Isabelle Dautriche, David Embick, Fred Lerdahl, Pritty Patel-Grosz, David Poeppel, Philippe Schlenker	Formal Models at the Core.	Cogn. Sci.	2023	DBLP DOI BibTeX RDF
28	Théotime Balaguer, Olivier Simonin 0001, Isabelle Guérin Lassous, Isabelle Fantoni	Etat de l'art sur la co-simulation robotique et réseau des systèmes multi-robots.	JFSMA	2023	DBLP BibTeX RDF
28	David Amarantini, Isabelle Rieu, Giovanni Castelnovo, Frédérique Fluchère, Chloé Laurencin, Bertrand Degos, Aurélia Poujois, Alexandre Kreisler, Sophie Sangla, Mélissa Tir, Isabelle Benatru, Geneviève Blanchet-Fourcade, Dominique Guehl, Dominique Gayraud, Laurent Tatu, Christine Tranchant, Franck Durif, Marion Simonetta-Moreau	Quantification of Head Tremors in Medical Conditions: A Comparison of Analyses Using a 2D Video Camera and a 3D Wireless Inertial Motion Unit.	Sensors	2022	DBLP DOI BibTeX RDF
28	Mauro Florez, Jenny Melo, Isabelle Bourdon, Isabelle Piot-Lepetit, Karine Gauche	Digital Divide between Colombian and French Agriculture.	AMCIS	2021	DBLP BibTeX RDF
28	Margherita Volpe, Omar Veledar, Isabelle Chartier, Isabelle Dor, Fredy Ríos Silva, Jure Trilar, Csaba Király 0002, Gabriele Gaffuri, Sabine Hafner-Zimmermann	Experimentation of Cross-Border Digital Innovation Hubs (DIHs) Cooperation and Impact on SME Services.	PRO-VE	2021	DBLP DOI BibTeX RDF
28	Richard Philip Kipling, Cairistiona F. E. Topp, André Bannink, David J. Bartley, Isabel Blanco-Penedo, Raffaele Cortignani, Agustin del Prado, Gabriele Dono, Philippe Faverdin, Anne-Isabelle Graux, Nicholas J. Hutchings, Ludwig Lauwers, Seyda Özkan Gülzari, Pytrik Reidsma, Susanne Rolinski, Margarita Ruiz-Ramos, Daniel L. Sandars, Renata Sándor, Martin Schönhart, Giovanna Seddaiu, Jantine van Middelkoop, Shailesh Shrestha, Isabelle Weindl, Vera Eory	To what extent is climate change adaptation a novel challenge for agricultural modellers?	Environ. Model. Softw.	2019	DBLP DOI BibTeX RDF
28	Gilgueng Hwang, Rémy Braive, Laurent Couraud, Antonella Cavanna, Ouerghi Abdelkarim, Isabelle Robert-Philip, Alexios Beveratos, Isabelle Sagnes, D. Sinan Haliyo, Stephane Régnier	Electro-osmotic propulsion of helical nanobelt swimmers.	Int. J. Robotics Res.	2011	DBLP DOI BibTeX RDF
28	Xavier Moles Lopez, Olivier Debeir, Calliope Maris, Isabelle Roland, Isabelle Salmon, Christine Decaestecker	KI-67 hot-spots detection on glioblastoma tissue sections.	ISBI	2010	DBLP DOI BibTeX RDF
28	Sébastien Treserras, Kader Boulanouar, Fabrice Conchou, Marion Simonetta-Moreau, Isabelle Berry, Pierre Celsis, François Chollet, Isabelle Loubinoux	Transition from rest to movement: Brain correlates revealed by functional connectivity.	NeuroImage	2009	DBLP DOI BibTeX RDF
28	Isabelle Merlet, Philippe Ryvlin, Nicolas Costes 0001, Damien Dufournel, Jean Isnard, Isabelle Faillenot, Karine Ostrowsky, Franck Lavenne, Didier Le Bars, François Mauguière	Statistical parametric mapping of 5-HT1A receptor binding in temporal lobe epilepsy with hippocampal ictal onset on intracranial EEG.	NeuroImage	2004	DBLP DOI BibTeX RDF