Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
58 | Marcel Oliveira, Ana Cavalcanti 0001, Jim Woodcock 0001 |
Unifying Theories in ProofPower-Z. ![Search on Bibsonomy](Pics/bibsonomy.png) |
UTP ![In: Unifying Theories of Programming, First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006, Revised Selected Papers, pp. 123-140, 2006, Springer, 3-540-34750-X. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Unifying Theories of Programming, theorem prover |
58 | Vincent Zammit |
On the Implementation of an Extensible Declarative Proof Language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings, pp. 185-202, 1999, Springer, 3-540-66463-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
58 | Vincent Zammit |
A Comparative Study of Coq and HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, pp. 323-337, 1997, Springer, 3-540-63379-0. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
50 | Wing Lam, Sara Jones 0001 |
Mechanising Requirements Engineering: Reuse and the Application of Domain Analysis Technology. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASE ![In: 1997 International Conference on Automated Software Engineering, ASE 1997, Lake Tahoe, CA, USA, November 2-5, 1997, pp. 303-304, 1997, IEEE Computer Society, 0-8186-7961-1. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
requirements engineering mechanisation, domain analysis technology, industrial avionics domain, application domain analysis, task domain analysis, formal specification, reuse |
49 | Andrew D. Gordon 0001 |
A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HUG ![In: Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings, pp. 413-425, 1993, Springer, 3-540-57826-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
31 | Eerke A. Boiten, John Derrick, Gerhard Schellhorn |
Relational concurrent refinement part II: Internal operations and outputs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 21(1-2), pp. 65-102, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Process algebraic semantics, Failures-divergences refinement, Internal operations, Mechanisation, KIV, Simulations, Deadlock, Z, Data refinement, Outputs |
31 | Michael Jackson 0001 |
Automated software engineering: supporting understanding. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Autom. Softw. Eng. ![In: Autom. Softw. Eng. 15(3-4), pp. 275-281, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Mechanisation, Complexity, Automation, Fragmentation, Manipulation, Description |
30 | Hongying Wang, Bing Sun |
Mechanisation and path analysis of dominant technology in emerging energy industry - based on CA model and fsQCA method. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Technol. Manag. ![In: Int. J. Technol. Manag. 92(4), pp. 329-345, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
30 | Hing-Lun Chan, Michael Norrish |
Mechanisation of the AKS Algorithm. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 65(2), pp. 205-256, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
30 | Uma Zalakain, Ornela Dardha |
π with Leftovers: A Mechanisation in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FORTE ![In: Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings, pp. 157-174, 2021, Springer, 978-3-030-78088-3. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
30 | Chengdai Huang, Jinde Cao |
Bifurcation Mechanisation of a Fractional-Order Neural Network with Unequal Delays. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Neural Process. Lett. ![In: Neural Process. Lett. 52(2), pp. 1171-1187, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
30 | Uma Zalakain, Ornela Dardha |
π with leftovers: a mechanisation in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2005.05902, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
30 | Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber |
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP ![In: Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020., pp. 1-17, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
30 | Daniela Lovarelli, Marco Fiala, Gunnar Larsson |
Fuel consumption and exhaust emissions during on-field tractor activity: A possible improving strategy for the environmental load of agricultural mechanisation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. Electron. Agric. ![In: Comput. Electron. Agric. 151, pp. 238-248, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
30 | Andrea Mannocci, Angelo Antonio Salatino, Francesco Osborne, Enrico Motta |
2100 AI: Reflections on the Mechanisation of Scientific Discovery. ![Search on Bibsonomy](Pics/bibsonomy.png) |
BlackMirror@ISWC ![In: Proceedings of the Re-coding Black Mirror 2017 Workshop co-located with 16th International Semantic Web Conference (ISWC 2017), Vienna, Austria, October 22, 2017., 2017, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP BibTeX RDF |
|
30 | Hing-Lun Chan, Michael Norrish |
Mechanisation of AKS Algorithm: Part 1 - The Main Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, pp. 117-136, 2015, Springer, 978-3-319-22101-4. The full citation details ...](Pics/full.jpeg) |
2015 |
DBLP DOI BibTeX RDF |
|
30 | Seyed H. Haeri |
Component-based mechanisation of programming languages in embedded settings. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2015 |
RDF |
|
30 | Aditi Barthwal, Michael Norrish |
A mechanisation of some context-free language theory in HOL4. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Comput. Syst. Sci. ![In: J. Comput. Syst. Sci. 80(2), pp. 346-362, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
30 | Seyed H. Haeri, Sibylle Schupp |
Reusable Components for Lightweight Mechanisation of Programming Languages. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SC@STAF ![In: Software Composition - 12th International Conference, SC@STAF 2013, Budapest, Hungary, June 19, 2013. Proceedings, pp. 1-16, 2013, Springer, 978-3-642-39613-7. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
30 | Matthew J. Lovert |
On the mechanisation of the logic of partial functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2013 |
RDF |
|
30 | Manfred Kerber, Michael Kohlhase |
Reasoning without believing: on the mechanisation of presuppositions and partiality. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Appl. Non Class. Logics ![In: J. Appl. Non Class. Logics 22(4), pp. 295-317, 2012. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
30 | Aditi Barthwal, Michael Norrish |
Mechanisation of PDA and Grammar Equivalence for Context-Free Languages. ![Search on Bibsonomy](Pics/bibsonomy.png) |
WoLLIC ![In: Logic, Language, Information and Computation, 17th International Workshop, WoLLIC 2010, Brasilia, Brazil, July 6-9, 2010. Proceedings, pp. 125-135, 2010, Springer, 978-3-642-13823-2. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
30 | Howard Rosenbrock |
Ethics, science, and the mechanisation of the world picture. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AI Soc. ![In: AI Soc. 18(1), pp. 7-20, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
Taylorism, Work design, Causality, Purpose, Quantum theory |
30 | David John Clark |
Enclosing the field : from 'mechanisation of thought processes' to 'autonomics'. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2002 |
RDF |
|
30 | René Vestergaard, James Brotherston |
The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective). ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Mechanized Reasoning about Languages with Variable Binding, MERLIN 2001, in connection with IJCAR 2001, Siena, Italy, June 18, 2001, pp. 18-36, 2001, Elsevier. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
30 | Jeremy E. Dawson, Rajeev Goré |
A Mechanisation of Classical Modal Tense Logics Using Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Australian Joint Conference on Artificial Intelligence ![In: Advanced Topics in Artificial Intelligence, 11th Australian Joint Conference on Artificial Intelligence, AI '98, Brisbane, Australia, July 13-17, 1998, Selected Papers, pp. 107-118, 1998, Springer, 3-540-65138-1. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
logics for knowledge and belief, display logic, sequent calculus, automated deduction, hybrid logics, tense logic |
30 | Vincent Zammit |
A Mechanisation of Computability Theory in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings, pp. 431-446, 1996, Springer, 3-540-61587-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
30 | William L. Harrison, Myla Archer, Karl N. Levitt |
A HOL Mechanisation of the Axiomatic Semantics of a Simple Distributed Programming Language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92, Leuven, Belgium, 21-24 September 1992, pp. 347-356, 1992, North-Holland/Elsevier, 0-444-89880-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
30 | Andrew Stevens 0001 |
An improved method for the mechanisation of inductive proof. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1989 |
RDF |
|
30 | P. Seetharamaiah, V. R. Murthy |
Tabular Mechanisation for Flexible Testing of Microprocessors. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITC ![In: Proceedings International Test Conference 1986, Washington, D.C., USA, September 1986, pp. 394-407, 1986, IEEE Computer Society. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP BibTeX RDF |
|
19 | Harvey Tuch |
Formal Verification of C Systems Code. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 42(2-4), pp. 125-187, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
C, Separation logic, Interactive theorem proving |
19 | Marcel Oliveira, Ana Cavalcanti 0001, Jim Woodcock 0001 |
A UTP semantics for Circus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 21(1-2), pp. 3-32, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Concurrency, Theorem proving, Relational model, Refinement calculus |
19 | Aditi Barthwal, Michael Norrish |
Verified, Executable Parsing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESOP ![In: Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, pp. 160-174, 2009, Springer, 978-3-642-00589-3. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
19 | Frank Zeyda, Ana Cavalcanti 0001 |
Mechanised Translation of Control Law Diagrams into Circus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFM ![In: Integrated Formal Methods, 7th International Conference, IFM 2009, Düsseldorf, Germany, February 16-19, 2009. Proceedings, pp. 151-166, 2009, Springer, 978-3-642-00254-0. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
ClawZ, verification, CSP, Z, Simulink |
19 | Leo Freitas |
Mechanising Data-Types for Kernel Design in Z. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SBMF ![In: Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009, Revised Selected Papers, pp. 186-203, 2009, Springer, 978-3-642-10451-0. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
19 | Alexei Iliasov |
Refinement patterns for rapid development of dependable systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EFTS ![In: Proceedings of the 2007 Workshop on Engineering Fault Tolerant Systems, EFTS 2007, Dubrovnik, Croatia, September 4, 2007, pp. 10, 2007, ACM, 978-1-59593-725-4. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
19 | Leo Freitas, Zheng Fu, Jim Woodcock 0001 |
POSIX file store in Z/Eves: an experiment in the verified software repository. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICECCS ![In: 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 10-14 July 2007, Auckland, New Zealand, pp. 3-14, 2007, IEEE Computer Society, 978-0-7695-2895-3. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
19 | Michael Norrish |
Mechanising lambda-calculus using a classical first order theory of terms with permutations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
High. Order Symb. Comput. ![In: High. Order Symb. Comput. 19(2-3), pp. 169-195, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
19 | Annabelle McIver, Tjark Weber |
Towards Automated Proof Support for Probabilistic Distributed Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings, pp. 534-548, 2005, Springer, 3-540-30553-X. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
19 | Michael Norrish |
Mechanising Hankin and Barendregt using the Gordon-Melham axioms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
higher order abstract syntax, interactive theorem-proving |
19 | Linas Laibinis, Joakim von Wright |
Functional Procedures in Higher-Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 372-387, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
19 | Monica Nesi |
Formalising a Value-Passing Calculus in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 11(2), pp. 160-199, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
Meta-theoretic reasoning, Formal verification, Theorem proving, Higher order logic, Process calculi |
19 | Jacques D. Fleuriot, Lawrence C. Paulson |
Proving Newton's Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Automated Deduction in Geometry ![In: Automated Deduction in Geometry, Second International Workshop, ADG'98, Beijing, China, August 1-3, 1998, Proceedings, pp. 47-66, 1998, Springer, 3-540-66672-9. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
19 | Clare Dixon, Michael Fisher 0001 |
The Set of Support Strategy in Temporal Resolution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TIME ![In: 5th Workshop on Temporal Representation and Reasoning, TIME '98, Sanibel Island, Florida, USA, May 16-17, 1998, pp. 113-120, 1998, IEEE Computer Society, 0-8186-8473-9. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
19 | Jeremy E. Dawson, Rajeev Goré |
A Mechanised Proof System for Relation Algebra using Display Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
JELIA ![In: Logics in Artificial Intelligence, European Workshop, JELIA '98, Dagstuhl, Germany, October 12-15, 1998, Proceedings, pp. 264-278, 1998, Springer, 3-540-65141-1. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
19 | Daniel Hirschkoff |
A Full Formalisation of pi-Calculus Theory in the Calculus of Constructions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, pp. 153-169, 1997, Springer, 3-540-63379-0. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
19 | Clare Dixon |
Search Strategies for Resolution in Temporal Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings, pp. 673-687, 1996, Springer, 3-540-61511-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|