article

Free access

Foundational aspects of syntax

Authors:

Dale Miller,

Catuscia PalmidessiAuthors Info & Claims

ACM Computing Surveys (CSUR), Volume 31, Issue 3es

Pages 11 - es

https://doi.org/10.1145/333580.333590

Published: 01 September 1999 Publication History

PDF eReader

References

[1]

Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56-68, 1940.

Google Scholar

[2]

J. F. Groote and F. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100:202-260, 1992.

Crossref

Google Scholar

[3]

Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, 1993.

Crossref

Google Scholar

[4]

Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497-536, 1991.

Google Scholar

[5]

Raymond McDowell. Reasoning in a Logic with Definitions and Induction. PhD thesis, University of Pennsylvania, December 1997.

Crossref

Google Scholar

[6]

Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax. In Glynn Winskel, editor, Proceedings of teh 1997 Symposium on Logic and Computer Science, 1997.

Crossref

Google Scholar

[7]

Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In Seif Haridi, editor, IEEE Symposium on Logic Programming, 379-388, San Francisco, 1987.

Google Scholar

[8]

Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125-157, 1991.

Google Scholar

[9]

Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, Part II. Information and Computation, pages 41-77, September 1992.

Crossref

Google Scholar

[10]

Tobias Nipkow. Higher-order critical pairs. In G. Kahn, editor, Sixth Annual Symposium on Logic in Computer Science, pages 342-349. IEEE, July 1991.

Google Scholar

[11]

Gopalan Nadathur and Dale Miller. An Overview of AProlog. In Fifth International Logic Programming Conference, pages 810-827, Seattle, Washington, August 1988. MIT Press.

Google Scholar

[12]

Gopalan Nadathur and Debra Sue Wilson. A Notation for Lambda Terms: A Generalization of Environments. Theoretical Computer Science 198(1-2): 49-98 (1998).

Crossref

Google Scholar

[13]

Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 361-386. Academic Press, 1990.

Google Scholar

[14]

Frank Pfenning and Conal Elliot. Higher-order abstract syntax. In Proceedings of the ACM- SIGPLAN Conference on Programming Language Design and Implementation,199- 208. ACM Press, 1988.

Crossref

Google Scholar

[15]

Frank Pfenning. Elf: A language for logic definition and verified metaprogramming. In Fourth Annual Symposium on Logic in Computer Science, pages 313-321, Monterey, CA, June 1989.

Crossref

Google Scholar

[16]

Zhenyu Qian. Linear unification of higher-order patterns. In J.-P. Jouannaud, editor, Proc. 1993 Coll. Trees in Algebra and Programming. Springer Verlag LNCS, 1993.

Crossref

Google Scholar

[17]

Davide Sangiorgi. 7r-calculus, internal mobility and agent-passing calculi. Theoretical Computer Science, 167(2):235-274, 1996.

Crossref

Google Scholar

Cited By

View all

Hu JPientka BSchöpp U(2022)A Category Theoretic View of Contextual Types: From Simple Types to Dependent TypesACM Transactions on Computational Logic10.1145/354511523:4(1-36)Online publication date: 20-Oct-2022
https://dl.acm.org/doi/10.1145/3545115
Felty AOlarte CXavier B(2021)A focused linear logical framework and its application to metatheory of object logicsMathematical Structures in Computer Science10.1017/S0960129521000323(1-29)Online publication date: 15-Nov-2021
https://doi.org/10.1017/S0960129521000323
Pientka BSchöpp U(2020)Semantical Analysis of Contextual TypesFoundations of Software Science and Computation Structures10.1007/978-3-030-45231-5_26(502-521)Online publication date: 17-Apr-2020
https://doi.org/10.1007/978-3-030-45231-5_26
Show More Cited By

Recommendations

Composing aspects with aspects
AOSD '10: Proceedings of the 9th International Conference on Aspect-Oriented Software Development

Aspect-oriented programming languages modularize crosscutting concerns by separating the concerns from a base program in aspects. What they do not modularize well is the code needed to manage interactions between the aspects themselves. Therefore ...
Abstract syntax notation two
Syntax Map: A Modeling Language for Capturing Requirements of Graphical DSML
APSEC '12: Proceedings of the 2012 19th Asia-Pacific Software Engineering Conference - Volume 01

Domain-specific modeling languages (DSMLs) are designed to model particular domains of interest using graphical, textual, or mixed syntax. Although most met modeling tools offer an environment that automates several language development tasks, there is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM Computing Surveys Volume 31, Issue 3es

Sept. 1999

77 pages

ISSN:0360-0300

EISSN:1557-7341

DOI:10.1145/333580

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 1999

Published in CSUR Volume 31, Issue 3es

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
793
Total Downloads

Downloads (Last 12 months)52
Downloads (Last 6 weeks)10

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Hu JPientka BSchöpp U(2022)A Category Theoretic View of Contextual Types: From Simple Types to Dependent TypesACM Transactions on Computational Logic10.1145/354511523:4(1-36)Online publication date: 20-Oct-2022
https://dl.acm.org/doi/10.1145/3545115
Felty AOlarte CXavier B(2021)A focused linear logical framework and its application to metatheory of object logicsMathematical Structures in Computer Science10.1017/S0960129521000323(1-29)Online publication date: 15-Nov-2021
https://doi.org/10.1017/S0960129521000323
Pientka BSchöpp U(2020)Semantical Analysis of Contextual TypesFoundations of Software Science and Computation Structures10.1007/978-3-030-45231-5_26(502-521)Online publication date: 17-Apr-2020
https://doi.org/10.1007/978-3-030-45231-5_26
Mahmoud MFelty A(2019)Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear LogicJournal of Automated Reasoning10.1007/s10817-019-09527-xOnline publication date: 22-Jun-2019
https://doi.org/10.1007/s10817-019-09527-x
MOMIGLIANO APIENTKA BTHIBODEAU D(2018)A case study in programming coinductive proofs: Howe’s methodMathematical Structures in Computer Science10.1017/S096012951800041529:8(1309-1343)Online publication date: 31-Oct-2018
https://doi.org/10.1017/S0960129518000415
Xavier BOlarte CReis GNigam V(2018)Mechanizing Focused Linear Logic in CoqElectronic Notes in Theoretical Computer Science10.1016/j.entcs.2018.10.014338(219-236)Online publication date: Oct-2018
https://doi.org/10.1016/j.entcs.2018.10.014
Miller D(2018)Mechanized Metatheory RevisitedJournal of Automated Reasoning10.1007/s10817-018-9483-3Online publication date: 4-Oct-2018
https://doi.org/10.1007/s10817-018-9483-3
FELTY AMOMIGLIANO APIENTKA B(2017)Benchmarks for reasoning with syntax trees containing binders and contexts of assumptionsMathematical Structures in Computer Science10.1017/S096012951700009328:09(1507-1540)Online publication date: 5-May-2017
https://doi.org/10.1017/S0960129517000093
Ferreira FPientka B(2017)Programs Using Syntax with First-Class BindersProgramming Languages and Systems10.1007/978-3-662-54434-1_19(504-529)Online publication date: 25-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54434-1_19
Chaudhuri KCimini MMiller DLeroy XTiu A(2015)A Lightweight Formalization of the Metatheory of Bisimulation-Up-ToProceedings of the 2015 Conference on Certified Programs and Proofs10.1145/2676724.2693170(157-166)Online publication date: 13-Jan-2015
https://dl.acm.org/doi/10.1145/2676724.2693170
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

References

Cited By

Recommendations

Composing aspects with aspects

Abstract syntax notation two

Syntax Map: A Modeling Language for Capturing Requirements of Graphical DSML

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations