|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 18 occurrences of 18 keywords
|
|
|
Results
Found 42 publication records. Showing 42 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
48 | Eric Deplagne, Claude Kirchner, Hélène Kirchner, Quang Huy Nguyen 0002 |
Proof Search and Proof Check for Equational and Inductive Theorems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings, pp. 297-316, 2003, Springer, 3-540-40559-3. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
proof terms, computation, induction, automated theorem proving, deduction, rewrite rules, proof assistant |
35 | Ruy J. G. B. de Queiroz |
On Reduction Rules, Meaning-as-use, and Proof-theoretic Semantics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Stud Logica ![In: Stud Logica 90(2), pp. 211-247, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
reduction rules, proof-terms, proof-theoretic semantics, game-theoretic semantics, dialogue semantics, natural deduction |
26 | Stefan Berghofer, Tobias Nipkow |
Proof Terms for Simply Typed 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. 38-52, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
18 | 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 |
18 | Frédéric Besson |
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, pp. 48-62, 2006, Springer, 978-3-540-74463-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
18 | Masami Hagiya |
Programming by Example and Proving by Example Using Higher-order Unification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 588-602, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
17 | Yuta Takahashi, Ryo Takemura |
Completeness of Second-Order Intuitionistic Propositional Logic with Respect to Phase Semantics for Proof-Terms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Philos. Log. ![In: J. Philos. Log. 48(3), pp. 553-570, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
17 | Christina Kohl, Aart Middeldorp |
Composing Proof Terms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, pp. 337-353, 2019, Springer, 978-3-030-29435-9. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
17 | Gabriel Ebner |
Fast Cut-Elimination using Proof Terms: An Empirical Study. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CL&C ![In: Proceedings Seventh International Workshop on Classical Logic and Computation, CL&C 2018, Oxford (UK), 7th of July 2018., pp. 24-38, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
17 | Franck Slama |
Automatic generation of proof terms in dependently typed programming languages. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2018 |
RDF |
|
17 | Herman Geuvers, Tonny Hurkens |
Proof Terms for Generalized Natural Deduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary, pp. 3:1-3:39, 2017, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-071-2. The full citation details ...](Pics/full.jpeg) |
2017 |
DBLP DOI BibTeX RDF |
|
17 | José Espírito Santo, Maria João Frade, Luís Pinto 0001 |
Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia, pp. 10:1-10:27, 2016, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-065-1. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
17 | Carlos Lombardi, Alejandro Ríos 0001, Roel de Vrijer |
Proof terms for infinitary rewriting, progress report. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1402.2245, 2014. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP BibTeX RDF |
|
17 | Carlos Lombardi, Alejandro Ríos 0001, Roel de Vrijer |
Proof Terms for Infinitary Rewriting. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA-TLCA ![In: Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, pp. 303-318, 2014, Springer, 978-3-319-08917-1. The full citation details ...](Pics/full.jpeg) |
2014 |
DBLP DOI BibTeX RDF |
|
17 | Ferruccio Guidi |
Procedural Representation of CIC Proof Terms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 44(1-2), pp. 53-78, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
17 | Claudio Sacerdoti Coen |
Declarative Representation of Proof Terms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 44(1-2), pp. 25-52, 2010. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
|
17 | Mitsuhiro Okada, Ryo Takemura |
Remarks on Semantic Completeness for Proof-Terms with Laird's Dual Affine/Intuitionistic lambda -Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Rewriting, Computation and Proof ![In: Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, pp. 167-181, 2007, Springer, 978-3-540-73146-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
17 | Eike Ritter, David J. Pym, Lincoln A. Wallen |
Proof-terms for classical and intuitionistic resolution. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Log. Comput. ![In: J. Log. Comput. 10(2), pp. 173-207, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
17 | Ken-etsu Fujita |
On Proof Terms and Embeddings of Classical Substructural Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Stud Logica ![In: Stud Logica 61(2), pp. 199-221, 1998. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
17 | Eike Ritter, David J. Pym, Lincoln A. Wallen |
Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract). ![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. 17-31, 1996, Springer, 3-540-61511-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
17 | Benjamin Grégoire, Jorge Luis Sacchini |
Combining a Verification Condition Generator for a Bytecode Language with Static Analyses. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TGC ![In: Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, pp. 23-40, 2007, Springer, 978-3-540-78662-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
17 | Fredrik Lindblad, Marcin Benke |
A Tool for Automated Theorem Proving in Agda. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, pp. 154-169, 2004, Springer, 3-540-31428-8. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
17 | Evan Goris |
Explicit Proofs in Formal Provability Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFCS ![In: Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, NY, USA, June 4-7, 2007, Proceedings, pp. 241-253, 2007, Springer, 978-3-540-72732-3. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
14 | Guillaume Melquiond |
Proving Bounds on Real-Valued Functions with Computations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, pp. 2-17, 2008, Springer, 978-3-540-71069-1. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
14 | Olivier Boite |
Proof Reuse with Extended Inductive Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings, pp. 50-65, 2004, Springer, 3-540-23017-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
14 | Alexandre Miquel, Benjamin Werner |
The Not So Simple Proof-Irrelevant Model of CC. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers, pp. 240-258, 2002, Springer, 3-540-14031-X. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
14 | Marko Luther |
More On Implicit Syntax. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, pp. 386-400, 2001, Springer, 3-540-42254-4. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
11 | Richard Bonichon, David Delahaye, Damien Doligez |
Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings, pp. 151-165, 2007, Springer, 978-3-540-75558-6. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Alexandre Miquel |
Classical Program Extraction in the Calculus of Constructions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, pp. 313-327, 2007, Springer, 978-3-540-74914-1. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
11 | Bruno Barras, Benjamin Grégoire |
On the Role of Type Decorations in the Calculus of Inductive Constructions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings, pp. 151-166, 2005, Springer, 3-540-28231-9. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Claudio Sacerdoti Coen |
Explanation in Natural Language of lamda-µµ-Terms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MKM ![In: Mathematical Knowledge Management, 4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers, pp. 234-249, 2005, Springer, 3-540-31430-X. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
11 | Einar Broch Johnsen, Christoph Lüth |
Theorem Reuse by Proof Term Transformation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings, pp. 152-167, 2004, Springer, 3-540-23017-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
8 | Peter W. O'Hearn |
Resource Interpretations, Bunched Implications and the alpha lambda-Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLCA ![In: Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings, pp. 258-279, 1999, Springer, 3-540-65763-0. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
8 | José Meseguer 0001, Carolyn L. Talcott |
A Partial Order Event Model for Concurrent Objects. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CONCUR ![In: CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings, pp. 415-430, 1999, Springer, 3-540-66425-4. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
8 | Shenwei Yu, Zhaohui Luo |
Implementing a Model Checker for LEGO. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FME ![In: FME '97: Industrial Applications and Strengthened Foundations of Formal Methods, 4th International Symposium of Formal Methods Europe, Graz, Austria, September 15-19, 1997, Proceedings, pp. 442-458, 1997, Springer, 3-540-63533-5. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
8 | Kentaro Kikuchi, Stéphane Lengrand |
Strong Normalisation of Cut-Elimination That Simulates beta-Reduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FoSSaCS ![In: Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings, pp. 380-394, 2008, Springer, 978-3-540-78497-5. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
8 | Tobias Nipkow |
Higher-Order Rewrite Systems (Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 6th International Conference, RTA-95, Kaiserslautern, Germany, April 5-7, 1995, Proceedings, pp. 256, 1995, Springer, 3-540-59200-8. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
5 | 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 |
|
5 | Anna Zamansky, Nissim Francez, Yoad Winter |
A 'Natural Logic' inference system using the Lambek calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Log. Lang. Inf. ![In: J. Log. Lang. Inf. 15(3), pp. 273-295, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Natural logic, Inference, Normalization, Lambek calculus |
5 | Limin Jia 0001, David Walker 0001 |
Modal Proofs as Distributed Programs (Extended Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESOP ![In: Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, pp. 219-233, 2004, Springer, 3-540-21313-9. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
5 | H. J. Sander Bruggink |
Residuals in Higher-Order Rewriting. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings, pp. 123-137, 2003, Springer, 3-540-40254-3. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
5 | Aleksandar Nanevski |
Meta-programming with names and necessity. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002., pp. 206-217, 2002, ACM, 1-58113-487-8. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
modal lambda-calculus, higher-order abstract syntax |
Displaying result #1 - #42 of 42 (100 per page; Change: )
|
|