Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
76 | Roberto F. Lu, Cliff J. Kirkham |
A Six Sigma DMADV project: The 787 LCF scheduling tool. ![Search on Bibsonomy](Pics/bibsonomy.png) |
WSC ![In: Proceedings of the 2008 Winter Simulation Conference, Global Gateway to Discovery, WSC 2008, InterContinental Hotel, Miami, Florida, USA, December 7-10, 2008, pp. 2927, 2008, WSC, 978-1-4244-2708-6. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
76 | Stefan Sokolowski |
Soundness of Hoare's Logic: An Automated Proof Using LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Program. Lang. Syst. ![In: ACM Trans. Program. Lang. Syst. 9(1), pp. 100-120, 1987. The full citation details ...](Pics/full.jpeg) |
1987 |
DBLP DOI BibTeX RDF |
|
50 | Paul E. Utgoff, Richard P. Cochran |
A Least-Certainty Heuristic for Selective Search. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Computers and Games ![In: Computers and Games, Second International Conference, CG 2000, Hamamatsu, Japan, October 26-28, 2000, Revised Papers, pp. 1-18, 2000, Springer, 3-540-43080-6. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
Selective search, evaluation function error, misordering assumption, evaluation goal, swing threshold, LCF, random trees, artificial time, confidence, certainty, swing, Amazons, Othello |
50 | Filipp Akopyan, Rajit Manohar, Alyssa B. Apsel |
A Level-Crossing Flash Asynchronous Analog-to-Digital Converter. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASYNC ![In: 12th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2006), 13-15 March 2006, Grenoble, France, pp. 12-22, 2006, IEEE Computer Society, 0-7695-2498-2. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
50 | Sriram Ramabhadran, George Varghese |
Efficient implementation of a statistics counter architecture. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SIGMETRICS ![In: Proceedings of the International Conference on Measurements and Modeling of Computer Systems, SIGMETRICS 2003, June 9-14, 2003, San Diego, CA, USA, pp. 261-271, 2003, ACM, 1-58113-664-1. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
statistics counter, router |
50 | Norihisa Suzuki |
Inferring Types in Smalltalk. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Conference Record of the Eighth Annual ACM Symposium on Principles of Programming Languages, Williamsburg, Virginia, USA, January 1981, pp. 187-199, 1981, ACM Press, 0-89791-029-X. The full citation details ...](Pics/full.jpeg) |
1981 |
DBLP DOI BibTeX RDF |
|
49 | Jürgen Rudolph, Eckart Weiß, Michael Forster |
Modeling of welded joints for design against fatigue. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Eng. Comput. ![In: Eng. Comput. 19(2-3), pp. 142-151, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
BEA, FEA, Local approaches, Low cycle fatigue (LCF), Strain-based approach, Structural and notch stresses, Modeling |
43 | Sten Agerholm |
LCF Examples in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings, pp. 1-16, 1994, Springer, 3-540-58450-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
43 | Donald Sannella, Rod M. Burstall |
Structured Theories in LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAAP ![In: CAAP'83, Trees in Algebra and Programming, 8th Colloquium, L'Aquila, Italy, March 9-11, 1983, Proceedings, pp. 377-391, 1983, Springer, 3-540-12727-5. The full citation details ...](Pics/full.jpeg) |
1983 |
DBLP DOI BibTeX RDF |
|
33 | Maxime Crochemore, Alessandra Gabriele, Filippo Mignosi, Mauriana Pesaresi |
On the Longest Common Factor Problem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IFIP TCS ![In: Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, September 7-10, 2008, Milano, Italy, pp. 143-155, 2008, Springer, 978-0-387-09679-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
33 | Samir Khuller, Yoo Ah Kim, Yung-Chun (Justin) Wan |
Broadcasting on networks of workstations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SPAA ![In: SPAA 2005: Proceedings of the 17th Annual ACM Symposium on Parallelism in Algorithms and Architectures, July 18-20, 2005, Las Vegas, Nevada, USA, pp. 279-288, 2005, ACM, 1-58113-986-1. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
approximation algorithms, multicasting, broadcasting |
33 | Dongmei Ren, Imad Rahal, William Perrizo |
A Vertical Outlier Detection Algorithm with Clusters as By-Product. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTAI ![In: 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2004), 15-17 November 2004, Boca Raton, FL, USA, pp. 22-29, 2004, IEEE Computer Society, 0-7695-2236-X. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
33 | Nils Gura, Hans Eberle |
The Least Choice First Scheduling Method for High-Speed Network Switche. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IPDPS ![In: 16th International Parallel and Distributed Processing Symposium (IPDPS 2002), 15-19 April 2002, Fort Lauderdale, FL, USA, CD-ROM/Abstracts Proceedings, 2002, IEEE Computer Society, 0-7695-1573-8. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
33 | Tsern-Huei Lee, Ying-Che Kuo |
Performance Evaluation of Combined Input Output Queued Switch with Finite Input and Output Buffers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICOIN (1) ![In: Information Networking, Wireless Communications Technologies and Network Applications, International Conference, ICOIN 2002, Cheju Island, Korea, January 30 - February 1, 2002, Revised Papers, Part I, pp. 203-214, 2002, Springer, 3-540-44256-1. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
33 | Franz Regensburger |
HOLCF: Higher Order Logic of Computable Functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and Its Applications, 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995, Proceedings, pp. 293-307, 1995, Springer, 3-540-60275-5. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
33 | Maxime Crochemore |
Longest Common Factor of Two Words. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TAPSOFT, Vol.1 ![In: TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, March 23-27, 1987, Volume 1: Advanced Seminar on Foundations of Innovative Software Development I and Colloquium on Trees in Algebra and Programming (CAAP'87), pp. 26-36, 1987, Springer, 3-540-17660-8. The full citation details ...](Pics/full.jpeg) |
1987 |
DBLP DOI BibTeX RDF |
|
26 | Meifang Chen, Fei Fan |
Application of LCF Model Based on Deep Learning in Campus Network Platforms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICISCAE ![In: 5th IEEE International Conference on Information Systems and Computer Aided Education, ICISCAE 2022, Dalian, China, September 23-25, 2022, pp. 113-117, 2022, IEEE, 978-1-6654-8122-9. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
26 | Dongzhe Xuan, Yanji Piao, Dechao Wang, Zhijun Quan |
Failure Simulation Study of Double-Layer Exhaust Manifold for Turbocharged Engine Under LCF & HCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APWeb/WAIM Workshops ![In: Web and Big Data. APWeb-WAIM 2022 International Workshops - KGMA 2022, SemiBDMA 2022, DeepLUDA 2022, Nanjing, China, November 25-27, 2022, Proceedings, pp. 125-137, 2022, Springer, 978-981-99-1353-4. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
26 | Yohann de Castro, Luca Mencarelli |
Forecasting Nonnegative Time Series via Sliding Mask Method (SMM) and Latent Clustered Forecast (LCF). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2102.05314, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
26 | Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel |
From LCF to Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1907.02836, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
26 | Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel |
From LCF to Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 31(6), pp. 675-698, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
26 | Panagiotis Charalampopoulos, Maxime Crochemore, Costas S. Iliopoulos, Tomasz Kociumaka, Solon P. Pissis, Jakub Radoszewski, Wojciech Rytter, Tomasz Walen |
Linear-Time Algorithm for Long LCF with k Mismatches. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1802.06369, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
26 | Panagiotis Charalampopoulos, Maxime Crochemore, Costas S. Iliopoulos, Tomasz Kociumaka, Solon P. Pissis, Jakub Radoszewski, Wojciech Rytter, Tomasz Walen |
Linear-Time Algorithm for Long LCF with k Mismatches. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPM ![In: Annual Symposium on Combinatorial Pattern Matching, CPM 2018, July 2-4, 2018 - Qingdao, China, pp. 23:1-23:16, 2018, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-074-3. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
26 | Phil Scott, Steven Obua, Jacques D. Fleuriot |
Bootstrapping LCF Declarative Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1703.05351, 2017. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP BibTeX RDF |
|
26 | |
Nominal LCF: A Language for Generic Proof. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1605.02142, 2016. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP BibTeX RDF |
|
26 | Stéphane Graham-Lengrand |
Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods - 22th International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013. Proceedings, pp. 149-156, 2013, Springer, 978-3-642-40536-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
26 | Cezary Kaliszyk, Alexander Krauss 0001 |
Scalable LCF-Style Proof Translation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pp. 51-66, 2013, Springer, 978-3-642-39633-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
26 | Sriipriya G |
Implementation methodology for using concurrent and collaborative approaches for theorem provers, with case studies of SAT and LCF style provers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2013 |
RDF |
|
26 | Anthony C. J. Fox |
LCF-Style Bit-Blasting in HOL4. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings, pp. 357-362, 2011, Springer, 978-3-642-22862-9. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
|
26 | Sascha Böhme, Tjark Weber |
Fast LCF-Style Proof Reconstruction for Z3. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, pp. 179-194, 2010, Springer, 978-3-642-14051-8. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
26 | Sa'ed Abed, Otmane Aït Mohamed |
LCF-style for Secure Verification Platform based on Multiway Decision Graphs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CIIA ![In: Proceedings of the 2nd Conférence Internationale sur l'Informatique et ses Applications (CIIA'09), Saida, Algeria, May 3-4, 2009, 2009, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP BibTeX RDF |
|
26 | Sa'ed Abed, Otmane Aït Mohamed |
LCF-style Platform based on Multiway Decision Graphs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
WFLP ![In: Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming, WFLP 2008, Siena, Italy, July 3-4, 2008, pp. 3-26, 2008, Elsevier. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
26 | Hasan Amjad |
LCF-Style Propositional Simplification with BDDs and SAT Solvers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 55-70, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
26 | Tjark Weber |
Integrating a SAT Solver with an LCF-style Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PDPAR@CAV ![In: Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, PDPAR@CAV 2005, Edinburgh, UK, July 12, 2005, pp. 67-78, 2005, Elsevier. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
26 | Jong Woung Park, Joon Woong Lee, Kyung Young Jhang |
A lane-curve detection based on an LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Pattern Recognit. Lett. ![In: Pattern Recognit. Lett. 24(14), pp. 2301-2313, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
26 | Joe Hurd |
An LCF-Style Interface between HOL and First-Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings, pp. 134-138, 2002, Springer, 3-540-43931-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
26 | Pascal Hitzler, Anthony Karel Seda |
VDM meets LCF: Domain-Theoretic and Topological Aspects of VDM. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IWFM ![In: 5th Irish Workshop on Formal Methods, IWFM 2001, Dublin, Ireland, 16-17 July 2001, 2001, BCS. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP BibTeX RDF |
|
26 | Mike Gordon |
From LCF to HOL: a short history. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proof, Language, and Interaction ![In: Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 169-186, 2000, The MIT Press, 978-0-262-16188-6. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP BibTeX RDF |
|
26 | Olaf Müller, Tobias Nipkow, David von Oheimb, Oscar Slotosch |
HOLCF=HOL+LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 9(2), pp. 191-223, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
26 | Dennis M. Volpano, Geoffrey Smith 0001 |
A Type Soundness Proof for Variables in LCF ML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Process. Lett. ![In: Inf. Process. Lett. 56(3), pp. 141-146, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
26 | Peter Kornerup, David W. Matula |
LCF: A Lexicagraphic Binary representation of the Rationals. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Univers. Comput. Sci. ![In: J. Univers. Comput. Sci. 1(7), pp. 484-503, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
26 | Sten Agerholm |
LCF Examples in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. J. ![In: Comput. J. 38(2), pp. 121-130, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
26 | Franz Regensburger |
HOLCF: eine konservative Erweiterung von HOL um LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1994 |
RDF |
|
26 | Lawrence C. Paulson |
Verifying the Unification Algorithm in LCF ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR cs.LO/9301101, 1993. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP BibTeX RDF |
|
26 | Konrad Slind |
Adding New Rules to an LCF-style Logic Implementation. ![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. 549-559, 1992, North-Holland/Elsevier, 0-444-89880-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
26 | Bard Bloom |
Can LCF be Topped? Flat Lattice Models of Typed lambda-Calculus ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Comput. ![In: Inf. Comput. 87(1/2), pp. 263-300, July/August 1990. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
26 | Rob Booth |
An Evaluation of the LCF Theorem Prover using LOTOS. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FORTE ![In: Formal Description Techniques, II, Proceedings of the IFIP TC/WG6.1 Second International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, FORTE'89, Vancouver, BC, Canada, 5-8 December, 1989, pp. 83-99, 1989, North-Holland, 0-444-88544-7. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP BibTeX RDF |
|
26 | Bard Bloom |
Can LCF Be Topped? Flat Lattice models of Typed Lambda Calculus (Preliminary Report) ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), Edinburgh, Scotland, UK, July 5-8, 1988, pp. 282-295, 1988, IEEE Computer Society, 0-8186-0853-6. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
|
26 | Lawrence C. Paulson |
Logic and computation - interactive proof with Cambridge LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1987 |
RDF |
|
26 | Maxime Crochemore |
Computing LCF in linear time. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Bull. EATCS ![In: Bull. EATCS 30, pp. 57-60, 1986. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP BibTeX RDF |
|
26 | Lawrence C. Paulson |
Verifying the Unification Algorithm in LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Sci. Comput. Program. ![In: Sci. Comput. Program. 5(2), pp. 143-169, 1985. The full citation details ...](Pics/full.jpeg) |
1985 |
DBLP DOI BibTeX RDF |
|
26 | Lawrence C. Paulson |
Lessons Learned from LCF: A Survey of Natural Deduction Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. J. ![In: Comput. J. 28(5), pp. 474-479, 1985. The full citation details ...](Pics/full.jpeg) |
1985 |
DBLP DOI BibTeX RDF |
|
26 | Lawrence C. Paulson |
Deriving Structural Induction in LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Semantics of Data Types ![In: Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27-29, 1984, Proceedings, pp. 197-214, 1984, Springer, 3-540-13346-1. The full citation details ...](Pics/full.jpeg) |
1984 |
DBLP DOI BibTeX RDF |
|
26 | Avra Cohn |
The Equivalence of Two Semantic Definitions: A Case Study in LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SIAM J. Comput. ![In: SIAM J. Comput. 12(2), pp. 267-285, 1983. The full citation details ...](Pics/full.jpeg) |
1983 |
DBLP DOI BibTeX RDF |
|
26 | Jacek Leszczylowski |
FP Systems in Edinburgh LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFPC ![In: Formalization of Programming Concepts, International Colloquium, Peniscola, Spain, April 19-25, 1981, Proceedings, pp. 374-386, 1981, Springer, 3-540-10699-5. The full citation details ...](Pics/full.jpeg) |
1981 |
DBLP DOI BibTeX RDF |
|
26 | Jacek Leszczylowski |
On Proving Laws of the Algebra of FP-Systems in Edinburgh LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AAAI ![In: Proceedings of the 1st Annual National Conference on Artificial Intelligence, Stanford University, CA, USA, August 18-21, 1980., pp. 84-86, 1980, AAAI Press/MIT Press, 0-262-51050-2. The full citation details ...](Pics/full.jpeg) |
1980 |
DBLP BibTeX RDF |
|
26 | Jacek Leszczylowski |
An Experiment with "Edinburgh LCF". ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 5th Conference on Automated Deduction, Les Arcs, France, July 8-11, 1980, Proceedings, pp. 170-181, 1980, Springer, 3-540-10009-1. The full citation details ...](Pics/full.jpeg) |
1980 |
DBLP DOI BibTeX RDF |
|
26 | Jacek Leszczylowski |
Edingburgh LCF Supporting FP Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
GI Jahrestagung ![In: GI - 10. Jahrestagung, Saarbrücken, 30. September - 2. Oktober 1980, Proceedings, pp. 430, 1980, Springer, 3-540-10388-0. The full citation details ...](Pics/full.jpeg) |
1980 |
DBLP DOI BibTeX RDF |
|
26 | Michael J. C. Gordon, Robin Milner, Christopher P. Wadsworth |
Edinburgh LCF ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1979 |
DOI RDF |
|
26 | Robin Milner |
LCF: A Way of Doing Proofs with a Machine. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MFCS ![In: Mathematical Foundations of Computer Science 1979, Proceedings, 8th Symposium, Olomouc, Czechoslovakia, September 3-7, 1979, pp. 146-159, 1979, Springer, 0-387-09526-8. The full citation details ...](Pics/full.jpeg) |
1979 |
DBLP DOI BibTeX RDF |
|
26 | Michael J. C. Gordon, Robin Milner, F. Lockwood Morris, Malcolm C. Newey, Christopher P. Wadsworth |
A Metalanguage for Interactive Proof in LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, pp. 119-130, 1978, ACM Press. The full citation details ...](Pics/full.jpeg) |
1978 |
DBLP DOI BibTeX RDF |
|
26 | Nasser Saheb-Djahromi |
Probabilistic LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MFCS ![In: Mathematical Foundations of Computer Science 1978, Proceedings, 7th Symposium, Zakopane, Poland, September 4-8, 1978, pp. 442-451, 1978, Springer, 0-387-08921-7. The full citation details ...](Pics/full.jpeg) |
1978 |
DBLP DOI BibTeX RDF |
|
26 | Gordon D. Plotkin |
LCF Considered as a Programming Language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 5(3), pp. 223-255, 1977. The full citation details ...](Pics/full.jpeg) |
1977 |
DBLP DOI BibTeX RDF |
|
26 | Luigia Carlucci Aiello, Mario Aiello, Richard W. Weyhrauch |
Pascal in LCF: Semantics and Examples of Proof. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 5(2), pp. 135-177, 1977. The full citation details ...](Pics/full.jpeg) |
1977 |
DBLP DOI BibTeX RDF |
|
17 | David C. J. Matthews, Makarius Wenzel |
Efficient parallel programming in Poly/ML and Isabelle/ML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DAMP ![In: Proceedings of the POPL 2010 Workshop on Declarative Aspects of Multicore Programming, DAMP 2010, Madrid, Spain, January 19, 2010, pp. 53-62, 2010, ACM, 978-1-60558-859-9. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
parallel standard ml, poly/ml, theorem proving applications, data parallelism, isabelle |
17 | Juan Chen 0002, Ravi Chugh, Nikhil Swamy |
Type-preserving compilation of end-to-end verification of security enforcement. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLDI ![In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10, 2010, pp. 412-423, 2010, ACM, 978-1-4503-0019-3. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
bytecode languages, compilers, authorization, functional programming, information flow, dependent types, security type systems, mobile code security |
17 | Peter V. Homeier |
The HOL-Omega Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 244-259, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
17 | John Harrison 0001 |
HOL Light: An Overview. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 60-66, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
17 | Sadaf R. Alam, Richard F. Barrett, Heike Jagode, Jeffery A. Kuehn, Stephen W. Poole, Ramanan Sankaran |
Impact of Quad-Core Cray XT4 System and Software Stack on Scientific Computation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Euro-Par ![In: Euro-Par 2009 Parallel Processing, 15th International Euro-Par Conference, Delft, The Netherlands, August 25-28, 2009. Proceedings, pp. 334-344, 2009, Springer, 978-3-642-03868-6. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
17 | Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond |
Combining Coq and Gappa for Certifying Floating-Point Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings, pp. 59-74, 2009, Springer, 978-3-642-02613-3. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
17 | Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow |
The Isabelle Framework. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 33-38, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
17 | Mike Gordon |
Twenty Years of Theorem Proving for HOLs Past, Present and Future. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 1-5, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
17 | Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon |
Proof producing synthesis of arithmetic and cryptographic hardware. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 19(3), pp. 343-362, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Cryptography, Compiling, Theorem proving, Hardware synthesis, High assurance |
17 | Makarius Wenzel, Burkhart Wolff |
Building Formal Method Tools in the Isabelle/Isar Framework. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 352-367, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
17 | Amine Chaieb, Makarius Wenzel |
Context Aware Calculation and Deduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Calculemus/MKM ![In: Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007, Proceedings, pp. 27-39, 2007, Springer, 978-3-540-73083-5. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
17 | Amine Chaieb, Tobias Nipkow |
Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic. ![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. 367-380, 2005, Springer, 3-540-30553-X. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
17 | Narottam Chand, Ramesh C. Joshi, Manoj Misra |
Broadcast Based Cache Invalidation and Prefetching in Mobile Environment. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HiPC ![In: High Performance Computing - HiPC 2004, 11th International Conference, Bangalore, India, December 19-22, 2004, Proceedings, pp. 410-419, 2004, Springer, 3-540-24129-9. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
17 | Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, Xin Yu |
MetaPRL - A Modular Logical Environment. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings, pp. 287-303, 2003, Springer, 3-540-40664-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
17 | John Harrison 0001 |
Formal Verification at Intel. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings, pp. 45-, 2003, IEEE Computer Society, 0-7695-1884-2. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
17 | Harald Räcke, Christian Sohler, Matthias Westermann |
Online Scheduling for Sorting Buffers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESA ![In: Algorithms - ESA 2002, 10th Annual European Symposium, Rome, Italy, September 17-21, 2002, Proceedings, pp. 820-832, 2002, Springer, 3-540-44180-8. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
17 | Christoph Kern, Tarik Ono-Tesfaye, Mark R. Greenstreet |
A light-weight framework for hardware verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Softw. Tools Technol. Transf. ![In: Int. J. Softw. Tools Technol. Transf. 3(3), pp. 286-313, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
Refinement, Theorem-proving, Timing verification, Switch-level models, SRT division |
17 | Dag Normann |
Definability of Total Objects in PCF and Related Calculi. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLCA ![In: Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings., pp. 4-5, 2001, Springer, 3-540-41960-8. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
17 | Michael J. C. Gordon |
Reachability Programming in HOL98 Using BDDs. ![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. 179-196, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
17 | John Harrison 0001 |
High-Level Verification Using Theorem Proving and Formalized Mathematics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, pp. 1-6, 2000, Springer, 3-540-67664-3. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
17 | Joe Hurd |
Integrating Gandalf and HOL. ![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. 311-322, 1999, Springer, 3-540-66463-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
17 | Manfred Broy, Ursula Hinkel, Tobias Nipkow, Christian Prehofer, Birgit Schieder |
Interpreter Verification for a Functional Language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSTTCS ![In: Foundations of Software Technology and Theoretical Computer Science, 14th Conference, Madras, India, December 15-17, 1994, Proceedings, pp. 77-88, 1994, Springer, 3-540-58715-2. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
17 | Konrad Slind |
AC Unification in HOL90. ![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. 436-449, 1993, Springer, 3-540-57826-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
17 | Andrzej Blikle |
Three-Valued Predicates for Software Specification and Validation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
VDM Europe ![In: VDM '88, VDM - The Way Ahead, 2nd VDM-Europe Symposium, Dublin, Ireland, September 11-16, 1988, Proceedings, pp. 243-266, 1988, Springer, 3-540-50214-9. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
|
17 | Alan Bundy |
The Use of Explicit Plans to Guide Inductive Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, pp. 111-120, 1988, Springer, 3-540-19343-X. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
inductive proofs, formal methods, planning, theorem proving, automatic programming, Proof plans |
17 | Gérard P. Huet |
Induction Principles Formalized in the Calculus of Constructions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TAPSOFT, Vol.1 ![In: TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, March 23-27, 1987, Volume 1: Advanced Seminar on Foundations of Innovative Software Development I and Colloquium on Trees in Algebra and Programming (CAAP'87), pp. 276-286, 1987, Springer, 3-540-17660-8. The full citation details ...](Pics/full.jpeg) |
1987 |
DBLP DOI BibTeX RDF |
|
17 | William L. Scherlis, Dana S. Scott |
Semantically Based Programming Tools (Summary). ![Search on Bibsonomy](Pics/bibsonomy.png) |
TAPSOFT, Vol.1 ![In: Mathematical Foundations of Software Development, Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT), Berlin, Germany, March 25-29, 1985, Volume 1: Colloquium on Trees in Algebra and Programming (CAAP'85), pp. 52-59, 1985, Springer, 3-540-15198-2. The full citation details ...](Pics/full.jpeg) |
1985 |
DBLP DOI BibTeX RDF |
|
17 | Finn Verner Jensen, Kim Guldstrand Larsen |
Recursively Defined Domains and Their Induction Principles. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSTTCS ![In: Foundations of Software Technology and Theoretical Computer Science, Fifth Conference, New Delhi, India, December 16-18, 1985, Proceedings, pp. 225-245, 1985, Springer, 3-540-16042-6. The full citation details ...](Pics/full.jpeg) |
1985 |
DBLP DOI BibTeX RDF |
|
17 | Peter Dybjer |
Domain Algebras. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICALP ![In: Automata, Languages and Programming, 11th Colloquium, Antwerp, Belgium, July 16-20, 1984, Proceedings, pp. 138-150, 1984, Springer, 3-540-13345-3. The full citation details ...](Pics/full.jpeg) |
1984 |
DBLP DOI BibTeX RDF |
|
17 | David A. Schmidt |
A Programming Notation for Tactical Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984, Proceedings, pp. 445-459, 1984, Springer, 3-540-96022-8. The full citation details ...](Pics/full.jpeg) |
1984 |
DBLP DOI BibTeX RDF |
|
17 | Ketan Mulmuley |
The Mechanization of Existence Proofs of Recursive Predicates. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984, Proceedings, pp. 460-475, 1984, Springer, 3-540-96022-8. The full citation details ...](Pics/full.jpeg) |
1984 |
DBLP DOI BibTeX RDF |
|