7 Search Results for "Hughes, John"

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.33
Compiling with Arrays

Authors: David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and recursion, arrays in linear algebra demand constant-time access and bulk operations. To bridge this gap, some languages represent arrays as (eager) functions instead of lists. In this paper, we connect this idea to a formal logical foundation by interpreting functions as the usual negative types from polarized type theory, and arrays as the corresponding dual positive version of the function type. Positive types are defined to have a single elimination form whose computational interpretation is pattern matching. Just like (positive) product types bind two variables during pattern matching, (positive) array types bind variables with multiplicity during pattern matching. We follow a similar approach for Booleans by introducing conditionally-defined variables. The positive formulation for the array type enables us to combine typed partial evaluation and common subexpression elimination into an elegant algorithm whose result enjoys a property we call maximal fission, which we argue can be beneficial for further optimizations. For this purpose, we present the novel intermediate representation indexed administrative normal form (A_{i}NF), which relies on the formal logical foundation of the positive formulation for the array type to facilitate maximal loop fission and subsequent optimizations. A_{i}NF is normal with regard to commuting conversion for both let-bindings and for-loops, leading to flat and maximally fissioned terms. We mechanize the translation and normalization from a simple surface language to A_{i}NF, establishing that the process terminates, preserves types, and produces maximally fissioned terms.
Cite as

David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini. Compiling with Arrays. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 33:1-33:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{richter_et_al:LIPIcs.ECOOP.2024.33,
  author =	{Richter, David and B\"{o}hler, Timon and Weisenburger, Pascal and Mezini, Mira},
  title =	{{Compiling with Arrays}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{33:1--33:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.33},
  URN =		{urn:nbn:de:0030-drops-208823},
  doi =		{10.4230/LIPIcs.ECOOP.2024.33},
  annote =	{Keywords: array languages, functional programming, domain-specific languages, normalization by evaluation, common subexpression elimination, polarity, positive function type, intrinsic types}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.14
The Performance Effects of Virtual-Machine Instruction Pointer Updates

Authors: M. Anton Ertl and Bernd Paysan

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
How much performance do VM instruction-pointer (IP) updates cost and how much benefit do we get from optimizing them away? Two decades ago it had little effect on the hardware of the day, but on recent hardware the dependence chain of IP updates can become the critical path on processors with out-of-order execution. In particular, this happens if the VM instructions are light-weight and the application programs are loop-dominated. The present work presents several ways of reducing or eliminating the dependence chains from IP updates, either by breaking the dependence chains with the loop optimization or by reducing the number of IP updates (the c and ci optimizations) or their latency (the b optimization). Some benchmarks see speedups from these optimizations by factors > 2 on most recent cores, while other benchmarks and older cores see more modest results, often in the speedup ranges 1.1-1.3.
Cite as

M. Anton Ertl and Bernd Paysan. The Performance Effects of Virtual-Machine Instruction Pointer Updates. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 14:1-14:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ertl_et_al:LIPIcs.ECOOP.2024.14,
  author =	{Ertl, M. Anton and Paysan, Bernd},
  title =	{{The Performance Effects of Virtual-Machine Instruction Pointer Updates}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{14:1--14:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.14},
  URN =		{urn:nbn:de:0030-drops-208634},
  doi =		{10.4230/LIPIcs.ECOOP.2024.14},
  annote =	{Keywords: virtual machine, interpreter, out-of-order execution}
}
Document
DOI: 10.4230/OASIcs.FMBC.2024.2
Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda

Authors: Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

Abstract
Blockchain systems comprise critical software that handle substantial monetary funds, rendering them excellent candidates for formal verification. One of their core components is the underlying ledger that does all the accounting: keeping track of transactions and their validity, etc. Unfortunately, previous theoretical studies are typically confined to an idealized setting, while specifications for real implementations are scarce; either the functionality is directly implemented without a proper specification, or at best an informal specification is written on paper. The present work expands beyond prior meta-theoretical investigations of the EUTxO model to encompass the full scale of the Cardano blockchain: our formal specification describes a hierarchy of modular transitions that covers all the intricacies of a realistic blockchain, such as fully expressive smart contracts and decentralized governance. It is mechanized in a proof assistant, thus enjoys a higher standard of rigor: type-checking prevents minor oversights that were frequent in previous informal approaches; key meta-theoretical properties can now be formally proven; it is an executable specification against which the implementation in production is being tested for conformance; and it provides firm foundations for smart contract verification. Apart from a safety net to keep us in check, the formalization also provides a guideline for the ledger design: one informs the other in a symbiotic way, especially in the case of state-of-the-art features like decentralized governance, which is an emerging sub-field of blockchain research that however mandates a more exploratory approach. All the results presented in this paper have been mechanized in the Agda proof assistant and are publicly available. In fact, this document is itself a literate Agda script and all rendered code has been successfully type-checked.
Cite as

Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell. Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{knispel_et_al:OASIcs.FMBC.2024.2,
  author =	{Knispel, Andre and Melkonian, Orestis and Chapman, James and Hill, Alasdair and J\"{a}\"{a}ger, Joosep and DeMeo, William and Norell, Ulf},
  title =	{{Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{2:1--2:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.2},
  URN =		{urn:nbn:de:0030-drops-198673},
  doi =		{10.4230/OASIcs.FMBC.2024.2},
  annote =	{Keywords: blockchain, distributed ledgers, UTxO, Cardano, formal verification, Agda}
}
Document
DOI: 10.4230/DagSemProc.04381.1
04381 Abstracts Collection – Dependently Typed Programming

Authors: Thorsten Altenkirch, Martin Hofmann, and John Hughes

Published in: Dagstuhl Seminar Proceedings, Volume 4381, Dependently Typed Programming (2005)

Abstract
From 12.09.04 to 17.09.04, the Dagstuhl Seminar 04381 ``Dependently Typed Programming'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Thorsten Altenkirch, Martin Hofmann, and John Hughes. 04381 Abstracts Collection – Dependently Typed Programming. In Dependently Typed Programming. Dagstuhl Seminar Proceedings, Volume 4381, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:DagSemProc.04381.1,
  author =	{Altenkirch, Thorsten and Hofmann, Martin and Hughes, John},
  title =	{{04381 Abstracts Collection – Dependently Typed Programming}},
  booktitle =	{Dependently Typed Programming},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4381},
  editor =	{Thorsten Altenkirch and Martin Hofmann and John Hughes},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04381.1},
  URN =		{urn:nbn:de:0030-drops-1864},
  doi =		{10.4230/DagSemProc.04381.1},
  annote =	{Keywords: dependently typed programming}
}
Document
DOI: 10.4230/DagSemProc.04381.2
Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory (Extended Version)

Authors: Anton Setzer and Peter Hancock

Published in: Dagstuhl Seminar Proceedings, Volume 4381, Dependently Typed Programming (2005)

Abstract
We reconsider the representation of interactive programs in dependent type theory that the authors proposed in earlier papers. Whereas in previous versions the type of interactive programs was introduced in an ad hoc way, it is here defined as a weakly final coalgebra for a general form of polynomial functor. The are two versions: in the first the interface with the real world is fixed, while in the second the potential interactions can depend on the history of previous interactions. The second version may be appropriate for working with specifications of interactive programs. We focus on command-response interfaces, and consider both client and server programs, that run on opposite sides such an interface. We give formation/introduction/elimination/equality rules for these coalgebras. These are explored in two dimensions: coiterative versus corecursive, and monadic versus non-monadic. We also comment upon the relationship of the corresponding rules with guarded induction. It turns out that the introduction rules are nothing but a slightly restricted form of guarded induction. However, the form in which we write guarded induction is not recursive equations (which would break normalisation – we show that type checking becomes undecidable), but instead involves an elimination operator in a crucial way.
Cite as

Anton Setzer and Peter Hancock. Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory (Extended Version). In Dependently Typed Programming. Dagstuhl Seminar Proceedings, Volume 4381, pp. 1-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)

Copy BibTex To Clipboard

@InProceedings{setzer_et_al:DagSemProc.04381.2,
  author =	{Setzer, Anton and Hancock, Peter},
  title =	{{Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory (Extended Version)}},
  booktitle =	{Dependently Typed Programming},
  pages =	{1--30},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2005},
  volume =	{4381},
  editor =	{Thorsten Altenkirch and Martin Hofmann and John Hughes},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.04381.2},
  URN =		{urn:nbn:de:0030-drops-1768},
  doi =		{10.4230/DagSemProc.04381.2},
  annote =	{Keywords: Dependently types programming , interactive programs , coalgebras , weakly final coalgebras , coiteration , corecursion , monad}
}
Document
DOI: 10.4230/DagSemRep.89
Functional Programming in the Real World (Dagstuhl Seminar 9420)

Authors: Robert Giegerich and John Hughes

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Robert Giegerich and John Hughes. Functional Programming in the Real World (Dagstuhl Seminar 9420). Dagstuhl Seminar Report 89, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1994)

Copy BibTex To Clipboard

@TechReport{giegerich_et_al:DagSemRep.89,
  author =	{Giegerich, Robert and Hughes, John},
  title =	{{Functional Programming in the Real World (Dagstuhl Seminar 9420)}},
  pages =	{1--22},
  ISSN =	{1619-0203},
  year =	{1994},
  type = 	{Dagstuhl Seminar Report},
  number =	{89},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.89},
  URN =		{urn:nbn:de:0030-drops-149776},
  doi =		{10.4230/DagSemRep.89},
}
Document
DOI: 10.4230/DagSemRep.36
Functional Languages: Compiler Technology and Parallelism (Dagstuhl Seminar 9213)

Authors: Werner Damm, Chris Hankin, and John Hughes

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Werner Damm, Chris Hankin, and John Hughes. Functional Languages: Compiler Technology and Parallelism (Dagstuhl Seminar 9213). Dagstuhl Seminar Report 36, pp. 1-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1992)

Copy BibTex To Clipboard

@TechReport{damm_et_al:DagSemRep.36,
  author =	{Damm, Werner and Hankin, Chris and Hughes, John},
  title =	{{Functional Languages: Compiler Technology and Parallelism (Dagstuhl Seminar 9213)}},
  pages =	{1--32},
  ISSN =	{1619-0203},
  year =	{1992},
  type = 	{Dagstuhl Seminar Report},
  number =	{36},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.36},
  URN =		{urn:nbn:de:0030-drops-149240},
  doi =		{10.4230/DagSemRep.36},
}
  • Refine by Author
  • 3 Hughes, John
  • 1 Altenkirch, Thorsten
  • 1 Böhler, Timon
  • 1 Chapman, James
  • 1 Damm, Werner
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 1 Agda
  • 1 Cardano
  • 1 Dependently types programming
  • 1 UTxO
  • 1 array languages
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 3 2024
  • 2 2005
  • 1 1992
  • 1 1994

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact