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. |
WSC |
2008 |
DBLP DOI BibTeX RDF |
|
76 | Stefan Sokolowski |
Soundness of Hoare's Logic: An Automated Proof Using LCF. |
ACM Trans. Program. Lang. Syst. |
1987 |
DBLP DOI BibTeX RDF |
|
50 | Paul E. Utgoff, Richard P. Cochran |
A Least-Certainty Heuristic for Selective Search. |
Computers and Games |
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. |
ASYNC |
2006 |
DBLP DOI BibTeX RDF |
|
50 | Sriram Ramabhadran, George Varghese |
Efficient implementation of a statistics counter architecture. |
SIGMETRICS |
2003 |
DBLP DOI BibTeX RDF |
statistics counter, router |
50 | Norihisa Suzuki |
Inferring Types in Smalltalk. |
POPL |
1981 |
DBLP DOI BibTeX RDF |
|
49 | Jürgen Rudolph, Eckart Weiß, Michael Forster |
Modeling of welded joints for design against fatigue. |
Eng. Comput. |
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. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
43 | Donald Sannella, Rod M. Burstall |
Structured Theories in LCF. |
CAAP |
1983 |
DBLP DOI BibTeX RDF |
|
33 | Maxime Crochemore, Alessandra Gabriele, Filippo Mignosi, Mauriana Pesaresi |
On the Longest Common Factor Problem. |
IFIP TCS |
2008 |
DBLP DOI BibTeX RDF |
|
33 | Samir Khuller, Yoo Ah Kim, Yung-Chun (Justin) Wan |
Broadcasting on networks of workstations. |
SPAA |
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. |
ICTAI |
2004 |
DBLP DOI BibTeX RDF |
|
33 | Nils Gura, Hans Eberle |
The Least Choice First Scheduling Method for High-Speed Network Switche. |
IPDPS |
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. |
ICOIN (1) |
2002 |
DBLP DOI BibTeX RDF |
|
33 | Franz Regensburger |
HOLCF: Higher Order Logic of Computable Functions. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
33 | Maxime Crochemore |
Longest Common Factor of Two Words. |
TAPSOFT, Vol.1 |
1987 |
DBLP DOI BibTeX RDF |
|
26 | Meifang Chen, Fei Fan |
Application of LCF Model Based on Deep Learning in Campus Network Platforms. |
ICISCAE |
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. |
APWeb/WAIM Workshops |
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). |
CoRR |
2021 |
DBLP BibTeX RDF |
|
26 | Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel |
From LCF to Isabelle/HOL. |
CoRR |
2019 |
DBLP BibTeX RDF |
|
26 | Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel |
From LCF to Isabelle/HOL. |
Formal Aspects Comput. |
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. |
CoRR |
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. |
CPM |
2018 |
DBLP DOI BibTeX RDF |
|
26 | Phil Scott, Steven Obua, Jacques D. Fleuriot |
Bootstrapping LCF Declarative Proofs. |
CoRR |
2017 |
DBLP BibTeX RDF |
|
26 | |
Nominal LCF: A Language for Generic Proof. |
CoRR |
2016 |
DBLP BibTeX RDF |
|
26 | Stéphane Graham-Lengrand |
Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture. |
TABLEAUX |
2013 |
DBLP DOI BibTeX RDF |
|
26 | Cezary Kaliszyk, Alexander Krauss 0001 |
Scalable LCF-Style Proof Translation. |
ITP |
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. |
|
2013 |
RDF |
|
26 | Anthony C. J. Fox |
LCF-Style Bit-Blasting in HOL4. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
26 | Sascha Böhme, Tjark Weber |
Fast LCF-Style Proof Reconstruction for Z3. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
26 | Sa'ed Abed, Otmane Aït Mohamed |
LCF-style for Secure Verification Platform based on Multiway Decision Graphs. |
CIIA |
2009 |
DBLP BibTeX RDF |
|
26 | Sa'ed Abed, Otmane Aït Mohamed |
LCF-style Platform based on Multiway Decision Graphs. |
WFLP |
2008 |
DBLP DOI BibTeX RDF |
|
26 | Hasan Amjad |
LCF-Style Propositional Simplification with BDDs and SAT Solvers. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
26 | Tjark Weber |
Integrating a SAT Solver with an LCF-style Theorem Prover. |
PDPAR@CAV |
2005 |
DBLP DOI BibTeX RDF |
|
26 | Jong Woung Park, Joon Woong Lee, Kyung Young Jhang |
A lane-curve detection based on an LCF. |
Pattern Recognit. Lett. |
2003 |
DBLP DOI BibTeX RDF |
|
26 | Joe Hurd |
An LCF-Style Interface between HOL and First-Order Logic. |
CADE |
2002 |
DBLP DOI BibTeX RDF |
|
26 | Pascal Hitzler, Anthony Karel Seda |
VDM meets LCF: Domain-Theoretic and Topological Aspects of VDM. |
IWFM |
2001 |
DBLP BibTeX RDF |
|
26 | Mike Gordon |
From LCF to HOL: a short history. |
Proof, Language, and Interaction |
2000 |
DBLP BibTeX RDF |
|
26 | Olaf Müller, Tobias Nipkow, David von Oheimb, Oscar Slotosch |
HOLCF=HOL+LCF. |
J. Funct. Program. |
1999 |
DBLP DOI BibTeX RDF |
|
26 | Dennis M. Volpano, Geoffrey Smith 0001 |
A Type Soundness Proof for Variables in LCF ML. |
Inf. Process. Lett. |
1995 |
DBLP DOI BibTeX RDF |
|
26 | Peter Kornerup, David W. Matula |
LCF: A Lexicagraphic Binary representation of the Rationals. |
J. Univers. Comput. Sci. |
1995 |
DBLP DOI BibTeX RDF |
|
26 | Sten Agerholm |
LCF Examples in HOL. |
Comput. J. |
1995 |
DBLP DOI BibTeX RDF |
|
26 | Franz Regensburger |
HOLCF: eine konservative Erweiterung von HOL um LCF. |
|
1994 |
RDF |
|
26 | Lawrence C. Paulson |
Verifying the Unification Algorithm in LCF |
CoRR |
1993 |
DBLP BibTeX RDF |
|
26 | Konrad Slind |
Adding New Rules to an LCF-style Logic Implementation. |
TPHOLs |
1992 |
DBLP BibTeX RDF |
|
26 | Bard Bloom |
Can LCF be Topped? Flat Lattice Models of Typed lambda-Calculus |
Inf. Comput. |
1990 |
DBLP DOI BibTeX RDF |
|
26 | Rob Booth |
An Evaluation of the LCF Theorem Prover using LOTOS. |
FORTE |
1989 |
DBLP BibTeX RDF |
|
26 | Bard Bloom |
Can LCF Be Topped? Flat Lattice models of Typed Lambda Calculus (Preliminary Report) |
LICS |
1988 |
DBLP DOI BibTeX RDF |
|
26 | Lawrence C. Paulson |
Logic and computation - interactive proof with Cambridge LCF. |
|
1987 |
RDF |
|
26 | Maxime Crochemore |
Computing LCF in linear time. |
Bull. EATCS |
1986 |
DBLP BibTeX RDF |
|
26 | Lawrence C. Paulson |
Verifying the Unification Algorithm in LCF. |
Sci. Comput. Program. |
1985 |
DBLP DOI BibTeX RDF |
|
26 | Lawrence C. Paulson |
Lessons Learned from LCF: A Survey of Natural Deduction Proofs. |
Comput. J. |
1985 |
DBLP DOI BibTeX RDF |
|
26 | Lawrence C. Paulson |
Deriving Structural Induction in LCF. |
Semantics of Data Types |
1984 |
DBLP DOI BibTeX RDF |
|
26 | Avra Cohn |
The Equivalence of Two Semantic Definitions: A Case Study in LCF. |
SIAM J. Comput. |
1983 |
DBLP DOI BibTeX RDF |
|
26 | Jacek Leszczylowski |
FP Systems in Edinburgh LCF. |
ICFPC |
1981 |
DBLP DOI BibTeX RDF |
|
26 | Jacek Leszczylowski |
On Proving Laws of the Algebra of FP-Systems in Edinburgh LCF. |
AAAI |
1980 |
DBLP BibTeX RDF |
|
26 | Jacek Leszczylowski |
An Experiment with "Edinburgh LCF". |
CADE |
1980 |
DBLP DOI BibTeX RDF |
|
26 | Jacek Leszczylowski |
Edingburgh LCF Supporting FP Systems. |
GI Jahrestagung |
1980 |
DBLP DOI BibTeX RDF |
|
26 | Michael J. C. Gordon, Robin Milner, Christopher P. Wadsworth |
Edinburgh LCF |
|
1979 |
DOI RDF |
|
26 | Robin Milner |
LCF: A Way of Doing Proofs with a Machine. |
MFCS |
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. |
POPL |
1978 |
DBLP DOI BibTeX RDF |
|
26 | Nasser Saheb-Djahromi |
Probabilistic LCF. |
MFCS |
1978 |
DBLP DOI BibTeX RDF |
|
26 | Gordon D. Plotkin |
LCF Considered as a Programming Language. |
Theor. Comput. Sci. |
1977 |
DBLP DOI BibTeX RDF |
|
26 | Luigia Carlucci Aiello, Mario Aiello, Richard W. Weyhrauch |
Pascal in LCF: Semantics and Examples of Proof. |
Theor. Comput. Sci. |
1977 |
DBLP DOI BibTeX RDF |
|
17 | 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 |
17 | Juan Chen 0002, Ravi Chugh, Nikhil Swamy |
Type-preserving compilation of end-to-end verification of security enforcement. |
PLDI |
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. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
17 | John Harrison 0001 |
HOL Light: An Overview. |
TPHOLs |
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. |
Euro-Par |
2009 |
DBLP DOI BibTeX RDF |
|
17 | Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond |
Combining Coq and Gappa for Certifying Floating-Point Programs. |
Calculemus/MKM |
2009 |
DBLP DOI BibTeX RDF |
|
17 | Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow |
The Isabelle Framework. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
17 | Mike Gordon |
Twenty Years of Theorem Proving for HOLs Past, Present and Future. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
17 | Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon |
Proof producing synthesis of arithmetic and cryptographic hardware. |
Formal Aspects Comput. |
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. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
17 | Amine Chaieb, Makarius Wenzel |
Context Aware Calculation and Deduction. |
Calculemus/MKM |
2007 |
DBLP DOI BibTeX RDF |
|
17 | Amine Chaieb, Tobias Nipkow |
Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
17 | Narottam Chand, Ramesh C. Joshi, Manoj Misra |
Broadcast Based Cache Invalidation and Prefetching in Mobile Environment. |
HiPC |
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. |
TPHOLs |
2003 |
DBLP DOI BibTeX RDF |
|
17 | John Harrison 0001 |
Formal Verification at Intel. |
LICS |
2003 |
DBLP DOI BibTeX RDF |
|
17 | Harald Räcke, Christian Sohler, Matthias Westermann |
Online Scheduling for Sorting Buffers. |
ESA |
2002 |
DBLP DOI BibTeX RDF |
|
17 | Christoph Kern, Tarik Ono-Tesfaye, Mark R. Greenstreet |
A light-weight framework for hardware verification. |
Int. J. Softw. Tools Technol. Transf. |
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. |
TLCA |
2001 |
DBLP DOI BibTeX RDF |
|
17 | Michael J. C. Gordon |
Reachability Programming in HOL98 Using BDDs. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
17 | John Harrison 0001 |
High-Level Verification Using Theorem Proving and Formalized Mathematics. |
CADE |
2000 |
DBLP DOI BibTeX RDF |
|
17 | Joe Hurd |
Integrating Gandalf and HOL. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
17 | Manfred Broy, Ursula Hinkel, Tobias Nipkow, Christian Prehofer, Birgit Schieder |
Interpreter Verification for a Functional Language. |
FSTTCS |
1994 |
DBLP DOI BibTeX RDF |
|
17 | Konrad Slind |
AC Unification in HOL90. |
HUG |
1993 |
DBLP DOI BibTeX RDF |
|
17 | Andrzej Blikle |
Three-Valued Predicates for Software Specification and Validation. |
VDM Europe |
1988 |
DBLP DOI BibTeX RDF |
|
17 | Alan Bundy |
The Use of Explicit Plans to Guide Inductive Proofs. |
CADE |
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. |
TAPSOFT, Vol.1 |
1987 |
DBLP DOI BibTeX RDF |
|
17 | William L. Scherlis, Dana S. Scott |
Semantically Based Programming Tools (Summary). |
TAPSOFT, Vol.1 |
1985 |
DBLP DOI BibTeX RDF |
|
17 | Finn Verner Jensen, Kim Guldstrand Larsen |
Recursively Defined Domains and Their Induction Principles. |
FSTTCS |
1985 |
DBLP DOI BibTeX RDF |
|
17 | Peter Dybjer |
Domain Algebras. |
ICALP |
1984 |
DBLP DOI BibTeX RDF |
|
17 | David A. Schmidt |
A Programming Notation for Tactical Reasoning. |
CADE |
1984 |
DBLP DOI BibTeX RDF |
|
17 | Ketan Mulmuley |
The Mechanization of Existence Proofs of Recursive Predicates. |
CADE |
1984 |
DBLP DOI BibTeX RDF |
|